The following pages link to Amir Pnueli (Q208770):
Displaying 43 items.
- Low dimensional hybrid systems -- decidable, undecidable, don't know (Q418141) (← links)
- Verification of multi-linked heaps (Q439948) (← links)
- Synthesis of Reactive(1) designs (Q439954) (← links)
- \textit{Once} and \textit{for all} (Q439961) (← links)
- TimeC: A time constraint language for ILP processor compilation (Q698076) (← links)
- The temporal logic of branching time (Q789895) (← links)
- Propositional dynamic logic of nonregular programs (Q792083) (← links)
- Adequate proof principles for invariance and liveness properties of concurrent programs (Q795497) (← links)
- Fair termination revisited - with delay (Q795499) (← links)
- A linear-history semantics for languages for distributed programming (Q796298) (← links)
- Translation and run-time validation of loop transformations (Q812060) (← links)
- Verification of multiprocess probabilistic protocols (Q1079944) (← links)
- The temporal semantics of concurrent programs (Q1143164) (← links)
- Completing the temporal picture (Q1176248) (← links)
- A direct algorithm for checking equivalence of LL(k) grammars (Q1238431) (← links)
- Backtracking in recursive computations (Q1238623) (← links)
- A proof method for cyclic programs (Q1242445) (← links)
- Proving partial order properties (Q1322161) (← links)
- Models for reactivity (Q1323323) (← links)
- Temporal proof methodologies for timed transition systems (Q1333273) (← links)
- Symmetric and economical solutions to the mutual exclusion problem in a distributed system (Q1348531) (← links)
- Reachability analysis of dynamical systems having piecewise-constant derivatives (Q1367528) (← links)
- Verification of clocked and hybrid systems (Q1579058) (← links)
- A compositional approach to CTL\(^*\) verification (Q1770366) (← links)
- A discrete-time UML semantics for concurrency and communication in safety-critical applications (Q1776580) (← links)
- Probabilistic verification (Q1803654) (← links)
- Deterministic propositional dynamic logic: finite models, complexity, and completeness (Q1839245) (← links)
- Decidable integration graphs. (Q1854273) (← links)
- Verification by augmented finitary abstraction (Q1854391) (← links)
- Erratum: ``Verification by augmented finitary abstraction'' (Q1854497) (← links)
- The small model property: How small can it be? (Q1854568) (← links)
- Control and data abstraction: The cornerstones of practical formal verification (Q1856157) (← links)
- The code validation tool (CVT). Automatic verification of a compilation process (Q1865858) (← links)
- Model checking and abstraction to the aid of parameterized systems (a survey) (Q1886449) (← links)
- On the learnability of infinitary regular sets (Q1892893) (← links)
- Bridging the gap between fair simulation and trace inclusion (Q2486398) (← links)
- Model checking with strong fairness (Q2505624) (← links)
- Marked directed graphs (Q2552879) (← links)
- Axiomatic approach to total correctness of programs (Q2561482) (← links)
- Complete Proof System for QPTL (Q4779585) (← links)
- A Sound and Complete Deductive System for CTL* Verification (Q5504119) (← links)
- Free tidal oscillations in rotating flat basins of the form of rectangles and of sectors of circles (Q5542757) (← links)
- Tides in oceans of the form of a cross (Q5542758) (← links)
