``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
From MaRDI portal
Publication:689297
DOI10.1016/0304-3975(93)90248-RzbMath0788.68094MaRDI QIDQ689297
Publication date: 2 June 1994
Published in: Theoretical Computer Science (Search for Journal in Brave)
transition systemsparallel programsinduction principlessemantic completenessnondeterministic programs
Related Items (58)
Algebras of modal operators and partial correctness ⋮ A generic framework for heap and value analyses of object-oriented programming languages ⋮ Reachability analysis via orthogonal sets of patterns ⋮ On abstract interpretation of mobile ambients ⋮ Why does Astrée scale up? ⋮ Strictness analysis and denotational abstract interpretation ⋮ Abstract domains for type juggling ⋮ Modular inference of subprogram contracts for safety checking ⋮ The quotient of an abstract interpretation ⋮ On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics ⋮ Inverse-limit and topological aspects of abstract interpretation ⋮ A global constraint for over-approximation of real-time streams ⋮ Discovering invariants via simple component analysis ⋮ The essence of constraint propagation ⋮ The powerset operator on abstract interpretations ⋮ Design of abstract domains using first-order logic ⋮ Abstract interpretation of database query languages ⋮ Control-flow analysis of function calls and returns by abstract interpretation ⋮ Grammar semantics, analysis and parsing by abstract interpretation ⋮ Towards a foundation for semantics in complete metric spaces ⋮ Runtime verification of embedded real-time systems ⋮ The algorithmic analysis of hybrid systems ⋮ On model checking multiple hybrid views ⋮ Strictness analysis via abstract interpretation for recursively defined types ⋮ A monotone framework for CCS ⋮ Numerical invariants through convex relaxation and max-strategy iteration ⋮ 3-valued abstraction: More precision at less cost ⋮ A lattice for abstract interpretation of dynamic (LISP-like) structures ⋮ ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs ⋮ A Case Study in Abstract Interpretation Based Program Transformation ⋮ Relational Analysis and Precision via Probabilistic Abstract Interpretation ⋮ Regular Model Checking using Widening Techniques ⋮ Verifying Multithreaded Recursive Programs with Integer Variables ⋮ Incompleteness of states w.r.t. traces in model checking ⋮ Transforming semantics by abstract interpretation ⋮ Measuring the confinement of probabilistic systems ⋮ Exact join detection for convex polyhedra and other numerical abstractions ⋮ A new look at the automatic synthesis of linear ranking functions ⋮ Widening and narrowing operators for abstract interpretation ⋮ Demand-driven interprocedural analysis for map-based abstract domains ⋮ A zonotopic framework for functional abstractions ⋮ Abstract Interpretation From a Denotational-semantics Perspective ⋮ Constructive Galois Connections ⋮ On the algebraic structure of declarative programming languages ⋮ Applications of polyhedral computations to the analysis and verification of hardware and software systems ⋮ Abstract interpretation of resolution-based semantics ⋮ The reduced relative power operation on abstract domains ⋮ A class of polynomially solvable range constraints for interval analysis without widenings ⋮ A semantic framework for the abstract model checking of tccp programs ⋮ On finite-state approximants for probabilistic computation tree logic ⋮ Parsing as abstract interpretation of grammar semantics ⋮ An abstract interpretation framework to reason on finite failure and other properties of finite and infinite computations. ⋮ What You Lose is What You Leak: Information Leakage in Declassification Policies ⋮ Extracting Program Logics From Abstract Interpretations Defined by Logical Relations ⋮ On Probabilistic Techniques for Data Flow Analysis ⋮ Bi-inductive Structural Semantics ⋮ Constructive design of a hierarchy of semantics of a transition system by abstract interpretation ⋮ Sometime = always + recursion \(\equiv\) always. On the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs
Cites Work
- ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
- Sometime = always + recursion \(\equiv\) always. On the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs
- First-order dynamic logic
- Countable nondeterminism and random assignment
- Is “sometime” sometimes better than “always”?
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
