Verification of Concurrent Systems with VerCors

DOI10.1007/978-3-319-07317-0_5zbMath1445.68131OpenAlexW1574577245MaRDI QIDQ5175776

Saeed Darabi, Marieke Huisman, Wojciech Mostowski, Stefan Blom, Marina Zaharieva-Stojanovski, Afshin Amighi

Publication date: 25 February 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-07317-0_5

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (3)

Flexible Correct-by-Construction Programming ⋮ VerCors ⋮ Verifying Whiley programs with Boogie

Uses Software

• Dafny
• ANTLR
• CUDA
• Eiffel
• JML
• Spec#
• OpenCL
• VCC
• Chalice
• VeriFast
• Boogie
• Smallfoot
• KIV
• GPUVerify
• jStar

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Resources, concurrency, and local reasoning
• Automatic verification of Java programs with dynamic frames
• An axiomatic proof technique for parallel programs
• Modular invariants for layered object structures
• Resource Protection Using Atomics
• The Relationship Between Separation Logic and Implicit Dynamic Frames
• Barriers in Concurrent Separation Logic
• Dafny: An Automatic Program Verifier for Functional Correctness
• Local Reasoning for Storable Locks and Threads
• Ten Years of Hoare's Logic: A Survey—Part I
• Permission-Based Separation Logic for Multithreaded Java Programs
• Separation logic and abstraction
• An axiomatic basis for computer programming

This page was built for publication: Verification of Concurrent Systems with VerCors