Decidability of invariant validation for paramaterized systems

DOI10.1007/3-540-36577-X_8MaRDI QIDQ4417916zbMATH OpenFDO

Authors Pascal Fontaine, E. Pascal Gribomont

Publication date 30 July 2003

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/2619/26190097.htm

Mathematics Subject Classification ID

Classical first-order logic (03B10) Decidability of theories and sets of sentences (03B25) Logic in computer science (03B70) Quantifier elimination, model completeness, and related topics (03C10) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Parametrized invariance for infinite state processes
• Reduction and quantifier elimination techniques for program validation
• Decidability of inferring inductive invariants
• Model checking in bits and pieces
• Symmetry and Completeness in the Analysis of Parameterized Systems

Cited in

(9)

• Decidable fragments of many-sorted logic
• Stratified guarded first-order transition systems
• On invariant synthesis for parametric systems
• Symbolic backward reachability with effectively propositional logic. Application to security policy analysis
• Decidability of inferring inductive invariants
• Combinations of Theories for Decidable Fragments of First-Order Logic
• Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
• Model checking in bits and pieces
• Reduction and quantifier elimination techniques for program validation

This page was built for publication: Decidability of invariant validation for paramaterized systems

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