KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS

DOI10.1007/978-3-319-21401-6_35zbMath1465.68174OpenAlexW1475796516MaRDI QIDQ3454119

Richard Bubel, Reiner Hähnle, Crystal Chang Din

Publication date: 2 December 2015

Published in: Automated Deduction - CADE-25 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-21401-6_35

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

A Dynamic Logic with Traces and Coinduction, Cost analysis for an actor-based workflow modelling language, Behavioural semantics for asynchronous components, Stateful Behavioral Types for Active Objects, Distributed Network Generation Based on Preferential Attachment in ABS, Scalable optimal deployment in the cloud of component-based applications using optimization modulo theory, mathematical programming and symmetry breaking, KeY-ABS

Uses Software

• ABS

Cites Work

• Unnamed Item
• Observable behavior of distributed systems: component reasoning for concurrent objects
• A proof technique for parallel programs
• Compositional reasoning about active objects with shared futures
• Monitors
• Analysis of Executable Software Models