Automatic generation of invariants and intermediate assertions
From MaRDI portal
Publication:1391929
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
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
Cites Work