Parameterized verification with automatically computed inductive assertions

DOI10.1007/3-540-44585-4_19MaRDI QIDQ4551152zbMATH OpenFDO

Authors Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Ying Xu, Lenore D. Zuck, Ying Xu

Publication date 4 September 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/2102/21020221

Mathematics Subject Classification ID

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

Recommendations

• Automatic deductive verification with invisible invariants
• Automatic verification of parameterized networks of processes
• Model checking and abstraction to the aid of parameterized systems (a survey)
• Model-checking and abstraction to the aid of parameterized systems
• Beyond parameterized verification

Cited in

(33)

• Approximated parameterized verification of infinite-state processes with global conditions
• Verifying programs in the calculus of inductive constructions
• Automatic generation of invariants and intermediate assertions
• Model checking and abstraction to the aid of parameterized systems (a survey)
• Efficient verification of imperative programs using auto2
• Formal verification of mobile robot protocols
• Compositional analysis for verification of parameterized systems
• Parameterised verification for multi-agent systems
• Automatic deductive verification with invisible invariants
• Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
• Local symmetry and compositional verification
• Model checking parameterized systems
• Synthesis of large dynamic concurrent programs from dynamic specifications
• Verification Constraint Problems with Strengthening
• Liveness by Invisible Invariants
• Automatic Verification of Directory-Based Consistency Protocols
• Verification of multi-linked heaps
• Automated inductive verification of parameterized protocols
• Verification of parametrized systems by dynamic induction on diagrams
• Parametrized invariance for infinite state processes
• Parametric systems: verification and synthesis
• View abstraction -- a tutorial (invited paper)
• Tools and Algorithms for the Construction and Analysis of Systems
• Handling Parameterized Systems with Non-atomic Global Conditions
• Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
• Monotonic Abstraction in Action
• Computer Aided Verification
• Tools and Algorithms for the Construction and Analysis of Systems
• Parameterized recursive refinement types for automated program verification
• Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification
• Lost in abstraction: monotonicity in multi-threaded programs
• Sound verification procedures for temporal properties of infinite-state systems
• Application of the trace assertion method to the specification, design, and verification of automaton programs

Describes a project that uses

Uses Software

• Chaff

This page was built for publication: Parameterized verification with automatically computed inductive assertions

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