scientific article; zbMATH DE number 1956575

MaRDI QIDQ4417916zbMATH OpenFDO

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

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)

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)

• Combinations of Theories for Decidable Fragments of First-Order Logic
• 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

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)