Automatic deductive verification with invisible invariants

DOI10.1007/3-540-45319-9_7MaRDI QIDQ2769579zbMATH OpenFDO

Authors Amir Pnueli, Sitvanit Ruah, Lenore D. Zuck

Publication date 5 February 2002

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2031/20310082

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Parameterized verification with automatically computed inductive assertions
• Computer Aided Verification
• Model-checking and abstraction to the aid of parameterized systems
• Beyond parameterized verification
• Automated inductive verification of parameterized protocols

Cited in

(36)

• Local proofs for global safety properties
• Model checking and abstraction to the aid of parameterized systems (a survey)
• Checking deadlock-freedom of parametric component-based systems
• Universal invariant checking of parametric systems with quantifier-free SMT reasoning
• Compositional verification of smart contracts through communication abstraction
• Specification and verification of concurrent programs through refinements
• Compositional analysis for verification of parameterized systems
• Verification of parametric concurrent systems with prioritised FIFO resource management
• Verification diagrams revisited: Disjunctive invariants for easy verification
• Automated formal analysis and verification: an overview
• Compositional reasoning
• Model checking parameterized systems
• Synthesis of large dynamic concurrent programs from dynamic specifications
• Invariants for Parameterised Boolean Equation Systems
• Liveness by Invisible Invariants
• Automatic Verification of Directory-Based Consistency Protocols
• Abstract Counterexamples for Non-disjunctive Abstractions
• Parameterized verification with automatically computed inductive assertions
• Parametrized invariance for infinite state processes
• Structural Invariants for the Verification of Systems with Parameterized Architectures
• View abstraction -- a tutorial (invited paper)
• Tools and Algorithms for the Construction and Analysis of Systems
• Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
• Theoretical Aspects of Computing - ICTAC 2004
• Computer Aided Verification
• Tools and Algorithms for the Construction and Analysis of Systems
• Deductive verification in decidable fragments with Ivy
• Verification of SMT systems with quantifiers
• Synthesizing history and prophecy variables for symbolic model checking
• Invariant checking for SMT-based systems with quantifiers
• Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification
• Regular model checking upside-down: an invariant-based approach
• The beauty of predicate automata
• Sound verification procedures for temporal properties of infinite-state systems
• Control of parameterized discrete event systems
• Invariants for parameterised Boolean equation systems

Describes a project that uses

Uses Software

• PVS
• STeP

This page was built for publication: Automatic deductive verification with invisible invariants

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