scientific article

zbMath0481.68019MaRDI QIDQ3939208

Zohar Manna, Amir Pnueli

Publication date: 1982

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

zbMATH Keywords

invariancelivenesssafetytemporal semanticsintermittent assertion methodeventualityinductive assertion method

Mathematics Subject Classification ID

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

Related Items (19)

Verification of multiprocess probabilistic protocols ⋮ A model and temporal proof system for networks of processes ⋮ A mechanically verified incremental garbage collector ⋮ Concerning the semantic consequence relation in first-order temporal logic ⋮ Communication in concurrent dynamic logic ⋮ Arithmetical axiomatization of first-order temporal logic ⋮ Formalizing process algebraic verifications in the calculus of constructions ⋮ A complete axiomatic characterization of first-order temporal logic of linear time ⋮ Time window temporal logic ⋮ Compositional verification of real-time systems with explicit clock temporal logic ⋮ Concurrent systems and inevitability ⋮ Temporal stream logic modulo theories ⋮ SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR ⋮ Unnamed Item ⋮ Semantic specification and verification of data flow diagrams ⋮ An introduction to compositional methods for concurrency and their application to real-time. ⋮ On-line algorithms for networks of temporal constraints ⋮ Simulation, reduction and preservation of correctness properties of parallel systems ⋮ Defining liveness

This page was built for publication: