SAL 2

DOI10.1007/978-3-540-27813-9_45MaRDI 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

• Model checking Z specifications using SAL
• Symbolic analysis of transition systems
• Z2SAL: a translation-based model checker for Z
• NuSMV 2: An OpenSource tool for symbolic model checking
• Symbolic model checking: \(10^{20}\) states and beyond

Cited in

(25)

• From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories
• Generalized rewrite theories, coherence completion, and symbolic methods
• SAL
• Salsa: Combining constraint solvers with BDDs for automatic invariant checking
• Symbolic analysis of transition systems
• The Statemate verification environment -- making it real
• Combining Model Checking and Deduction
• Synthesis of large dynamic concurrent programs from dynamic specifications
• Timeout and Calendar Based Finite State Modeling and Verification of Real-Time Systems
• Scaling up model-checking. A case-study
• An action-based approach to the formal specification and automatic analysis of business processes under authorization constraints
• Mechanization of an integrated approach: Shallow embedding into SAL/PVS
• p2b: A translation utility for linking Promela and symbolic model checking (tool paper)
• Model checking simulation rules for linearizability
• A decidable timeout-based extension of linear temporal logic
• Linear temporal logic symbolic model checking
• SO(10)À LA PATI–SALAM
• Model checking RAISE applicative specifications
• NuSMV 2: An OpenSource tool for symbolic model checking
• An overview of the mCRL2 toolset and its recent advances
• Z2SAL: a translation-based model checker for Z
• Alloy as a refactoring checker?
• A Logic-Based Approach to Combinatorial Testing with Constraints
• Computer Aided Verification
• Progress in certifying hardware model checking results

Describes a project that uses

Uses Software

• PVS

This page was built for publication: SAL 2

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