scientific article; zbMATH DE number 1956575

zbMATH Open1031.68049MaRDI QIDQ4417916FDOQ4417916

Authors: Pascal Fontaine, E. Pascal Gribomont 

Publication date: 30 July 2003

Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2619/26190097.htm

Title of this publication is not available (Why is that?)

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) 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)

Cited In (9)

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

This page was built for publication:

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