Computer Aided Verification

DOI10.1007/B98490MaRDI QIDQ5312938zbMATH OpenOpenAlexFDO

Authors Leonardo de Moura, Sam Owre, Harald Rueß, John Rushby, Natarajan Shankar, Maria Sorea, Ashish Tiwari

Publication date 25 August 2005

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

Full work available at URL https://doi.org/10.1007/b98490

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• ZB 2005: Formal Specification and Development in Z and B
• scientific article; zbMATH DE number 1670517
• Z2SAL: a translation-based model checker for Z
• scientific article; zbMATH DE number 1903365
• Symbolic model checking: \(10^{20}\) states and beyond

Cited in

(25)

• Generalized rewrite theories, coherence completion, and symbolic methods
• SO(10)À LA PATI–SALAM
• Progress in certifying hardware model checking results
• scientific article; zbMATH DE number 1903365 (Why is no real title available?)
• scientific article; zbMATH DE number 1670805 (Why is no real title available?)
• Z2SAL: a translation-based model checker for Z
• scientific article; zbMATH DE number 1949593 (Why is no real title available?)
• An action-based approach to the formal specification and automatic analysis of business processes under authorization constraints
• Computer Aided Verification
• Model checking simulation rules for linearizability
• Timeout and Calendar Based Finite State Modeling and Verification of Real-Time Systems
• A Logic-Based Approach to Combinatorial Testing with Constraints
• Alloy as a refactoring checker?
• SAL
• Linear temporal logic symbolic model checking
• Model checking RAISE applicative specifications
• scientific article; zbMATH DE number 1744965 (Why is no real title available?)
• scientific article; zbMATH DE number 1629964 (Why is no real title available?)
• Scaling up model-checking. A case-study
• Synthesis of large dynamic concurrent programs from dynamic specifications
• Combining Model Checking and Deduction
• From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories
• A decidable timeout-based extension of linear temporal logic
• scientific article; zbMATH DE number 1670517 (Why is no real title available?)
• An overview of the mCRL2 toolset and its recent advances

Describes a project that uses

Uses Software

• PVS

This page was built for publication: Computer Aided Verification

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