scientific article; zbMATH DE number 868107

MaRDI QIDQ4873991zbMATH OpenFDO

Authors Zohar Manna, Amir Pnueli

Publication date 21 April 1996

zbMATH Keywords

temporal logicverification of parameterized reactive programs

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic programming (68N17) Specification and verification (program logics, model checking, etc.) (68Q60)

Cited in

(32)

• Tool support for learning Büchi automata and linear temporal logic
• From Hilbert's program to a logic tool box
• Domain science and engineering from computer science to the sciences of informatics. I: Engineering
• Analysis of meeting protocols by formalisation, simulation, and verification
• Constructing invariants for hybrid systems
• Model checking abilities of agents: a closer look
• The complexity of agent design problems: Determinism and history dependence
• Compositional analysis of C/C++ programs with veriSoft
• Model checking with strong fairness
• Predicate diagrams for the verification of real-time systems
• Counter abstraction in the CSP/FDR setting
• Polycheck: dynamic verification of iteration space transformations on affine programs
• scientific article; zbMATH DE number 3881857 (Why is no real title available?)
• Symbolic execution of Reo circuits using constraint automata
• Kripke modelling and verification of temporal specifications of a multiple UAV system
• A decidability result for the model checking of infinite-state systems
• scientific article; zbMATH DE number 1538039 (Why is no real title available?)
• scientific article; zbMATH DE number 7364137 (Why is no real title available?)
• Program verification through characteristic formulae
• scientific article; zbMATH DE number 7056237 (Why is no real title available?)
• Simulation refinement for concurrency verification
• Analog property checkers: a DDR2 case study
• Parameterized recursive refinement types for automated program verification
• Doomed program points
• Collecting statistics over runtime executions
• Contracts for concurrency
• Beyond contracts for concurrency
• A criterion for atomicity revisited
• Change-of-bases abstractions for non-linear hybrid systems
• A mechanical analysis of program verification strategies
• Deductive verification of alternating systems
• Property-directed incremental invariant generation

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 Q4873991)