CESAR
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Partitioned PLTL model-checking for refined transition systems
- Before and after vacuity
- Local proofs for global safety properties
- Model checking for hybrid logic
- Sémantique asynchrone et comportements infinis en CPS
- Two normal form theorems for CSP programs
- Characterizing finite Kripke structures in propositional temporal logic
- Fairness and related properties in transition systems - a temporal logic to deal with fairness
- Control machines: A new model of parallelism for compositional specifications and their effective compilation
- An experience in proving regular networks of processes by modular model checking
- MCGP
- Synchrobench
- Zing
- ALGOL 68
- veriSoft
- rCOS
- CalFuzzer
- PREVAIL
- SLAM
- SPIN
- NuSMV
- LoLA
- Punf
- A theory of formal synthesis via inductive learning
- Supervisory control and reactive synthesis: a comparative introduction
- ARMC
- An axiomatic semantics for \(\mathsf{ioco} \underline{\mathsf{s}}\) conformance relation
- Using partial orders for the efficient verification of deadlock freedom and safety properties
- Model checking of systems with many identical timed processes
- Module checking
- Practical CTL* model checking: Should SPIN be extended?
- Is your model checker on time? On the complexity of model checking for timed modal logics
- Syntax-directed model checking of sequential programs
- NeVer
- From pre-historic to post-modern symbolic model checking
- Zap
- SCR
- ADL
- jSpin
- Java PathFinder
- Bandera
- Cadence SMV
- Dependences in strategy logic
- Roboop
- Vacuity in practice: temporal antecedent failure
- Bebop
- Motras
- TLC
- SATORI
- ConTest
- eVolCheck
- MIO Workbench
- dSPIN
- JPAX
- A sound and complete proof system for a unified temporal logic
- CCured
- MOPS
- Model-checking precision agriculture logistics: the case of the differential harvest
- Beyond vacuity: towards the strongest passing formula
- On the order of test goals in specification-based testing
- Fifty years of Hoare's logic
- Synthesizing adaptive test strategies from temporal logic specifications
- A novel approach to verifying context free properties of programs
- LTL2BA
- Logical vs. behavioural specifications
- Next-preserving branching bisimulation
- Compositional analysis for verification of parameterized systems
- Bounded model checking of infinite state systems
- JPF-SE
- Model checking and synthesis for branching multi-weighted logics
- Model checking of pushdown systems for projection temporal logic
- Properties of a predicate transformer of the VRS system
- Model checking with strong fairness
- Verifying untimed and timed aspects of the experimental batch plant
- UNITY
- Probabilistic temporal logics via the modal mu-calculus
- Structure-based deadlock checking of asynchronous circuits
- VaqTree
- Polynomial interrupt timed automata: verification and expressiveness
- A proof system for unified temporal logic
- RATSY
- On the unusual effectiveness of logic in computer science
- scientific article; zbMATH DE number 1670774 (Why is no real title available?)
- scientific article; zbMATH DE number 1670783 (Why is no real title available?)
- scientific article; zbMATH DE number 1670793 (Why is no real title available?)
- scientific article; zbMATH DE number 1693453 (Why is no real title available?)
- scientific article; zbMATH DE number 1705164 (Why is no real title available?)
- Solving parity games using an automata-based algorithm
- Mechanical software verification: high level control aspects from a user's perspective
- Automated formal analysis and verification: an overview
- ATL with strategy contexts: expressiveness and model checking
- Verification and refutation of probabilistic specifications via games
- rCOS: defining meanings of component-based software architectures
- Formal modelling, analysis and verification of hybrid systems
- Complete abstractions and subclassical modal logics
- Temporal normal form for linear temporal logic formulae
- Runtime verification of component-based systems
- Looper
- Introduction to model checking
- Temporal logic and fair discrete systems
This page was built for software: CESAR
