Automatic generation of invariants and intermediate assertions

DOI10.1016/S0304-3975(96)00191-0zbMath0902.68120OpenAlexW2045112813MaRDI QIDQ1391929

Zohar Manna, Nikolaj Bjørner, Anca Browne

Publication date: 23 July 1998

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(96)00191-0

zbMATH Keywords

temporal specifications

Mathematics Subject Classification ID

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

Related Items

A formalization of programs in first-order logic with a discrete linear order, Backward symbolic execution with loop folding, Some ways to reduce the space dimension in polyhedra computations, Computing polynomial program invariants, Automatic generation of inductive invariants from high-level microarchitectural models of communication fabrics, Subsequence Invariants, Deductive verification of alternating systems, Weakest Invariant Generation for Automated Addition of Fault-Tolerance, Simplification of boolean verification conditions, Deductive verification of real-time systems using STeP

Uses Software

• STeP

Cites Work

• Unnamed Item
• Statecharts: a visual formalism for complex systems
• Affine relationships among variables of a program
• On the mechanical derivation of loop invariants
• Logical analysis of programs