scientific article; zbMATH DE number 5194318

Publication date: 20 September 2007

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

program specification first-order logic axiom system propositional logic Peano arithmetic mathematical induction program verification program correctness Presburger arithmetic decidable logic equality theory arithmetic of integers with addition arithmetic of rational numbers with addition arithmetic of real numbers with addition and multiplication (elementary algebra)axiomatic theories for lists

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Research exposition (monographs, survey articles) pertaining to computer science (68-02) First-order arithmetic and fragments (03F30) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (46)

A symbolic programming approach to the rendezvous search problem ⋮ Łukasiewicz Games ⋮ Erratum to: ``Analyzing restricted fragments of the theory of linear arithmetic ⋮ Interpolation systems for ground proofs in automated deduction: a survey ⋮ Semantically-guided goal-sensitive reasoning: model representation ⋮ Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays ⋮ Combining Model Checking and Deduction ⋮ A deductive approach towards reasoning about algebraic transition systems ⋮ Modular inference of subprogram contracts for safety checking ⋮ Metalevel algorithms for variant satisfiability ⋮ Regular model checking revisited ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Keeping logic in the trivium of computer science: a teaching perspective ⋮ Spatial and timing properties in highway traffic ⋮ What else is undecidable about loops? ⋮ On algebraic array theories ⋮ Pointfree expression and calculation: From quantification to temporal logic ⋮ Logical reduction of metarules ⋮ Symbolic execution of Reo circuits using constraint automata ⋮ An instantiation scheme for satisfiability modulo theories ⋮ Efficient strategies for CEGAR-based model checking ⋮ Preface to the special issue ``SI: satisfiability modulo theories ⋮ Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars ⋮ SMT-based verification of data-aware processes: a model-theoretic approach ⋮ An approach to multicore parallelism using functional programming: a case study based on Presburger arithmetic ⋮ Property-directed incremental invariant generation ⋮ Satisfiability modulo theories and chiral heterotic string vacua with positive cosmological constant ⋮ Relating syntactic and semantic perturbations of hybrid automata ⋮ On Interpolation in Decision Procedures ⋮ Analyzing restricted fragments of the theory of linear arithmetic ⋮ Loop invariants ⋮ Inferring Loop Invariants Using Postconditions ⋮ Variant-Based Satisfiability in Initial Algebras ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ Satisfiability Procedures for Combination of Theories Sharing Integer Offsets ⋮ Unnamed Item ⋮ Conflict-driven satisfiability for theory combination: transition system and completeness ⋮ Colors Make Theories Hard ⋮ Metalevel Algorithms for Variant Satisfiability ⋮ A Survey of Satisfiability Modulo Theory ⋮ Theory decision by decomposition ⋮ Possible models computation and revision -- a practical approach ⋮ A Roadmap to Decidability ⋮ Inductive theorem proving based on tree grammars ⋮ Book review of: Daniel Kroening and Ofer Strichman, Decision procedures: an algorithmic point of view ⋮ On interpolation in automated theorem proving

Uses Software

Octagon

This page was built for publication: