Key-ABS: a deductive verification tool for the concurrent modelling language ABS

DOI10.1007/978-3-319-21401-6_35MaRDI QIDQ3454119zbMATH OpenOpenAlexFDO

Authors Crystal Chang Din, Richard Bubel, Reiner Hähnle

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

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

Recommendations

• Analysis of executable software models
• A dynamic logic for deductive verification of multi-threaded programs
• scientific article; zbMATH DE number 2087530
• Mechanical analysis of reliable communication in the alternating bit protocol using the Maude invariant analyzer tool
• scientific article; zbMATH DE number 1759367

Cites work

• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• A proof technique for parallel programs
• Analysis of executable software models
• Compositional reasoning about active objects with shared futures
• Monitors
• Observable behavior of distributed systems: component reasoning for concurrent objects

Cited in

(12)

• Stateful Behavioral Types for Active Objects
• Distributed network generation based on preferential attachment in ABS
• KeY-ABS
• Cost analysis for an actor-based workflow modelling language
• Modular analysis of distributed hybrid systems using post-regions
• Scalable optimal deployment in the cloud of component-based applications using optimization modulo theory, mathematical programming and symmetry breaking
• Integrating ADTs in KeY and Their Application to History-Based Reasoning
• Behavioural semantics for asynchronous components
• Analysis of executable software models
• Mechanical analysis of reliable communication in the alternating bit protocol using the Maude invariant analyzer tool
• Asynchronous Cooperative Contracts for Cooperative Scheduling
• A dynamic logic with traces and coinduction

Describes a project that uses

Uses Software

• ABS

This page was built for publication: Key-ABS: a deductive verification tool for the concurrent modelling language ABS

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3454119)