scientific article; zbMATH DE number 1798181
From MaRDI portal
Publication:4553254
Recommendations
Cited in
(43)- A compositional approach to CTL^* verification
- Certifying emptiness of timed Büchi automata
- Vacuity in practice: temporal antecedent failure
- Certifying proofs for SAT-based model checking
- TOrPEDO : witnessing model correctness with topological proofs
- A self-certifying compilation framework for WebAssembly
- From complementation to certification
- scientific article; zbMATH DE number 1670785 (Why is no real title available?)
- Certification for -calculus with winning strategies
- The Proof Certifier Checkers
- Implementing Spi Calculus Using Nominal Techniques
- Automatic Synthesis of Assumptions for Compositional Model Checking
- Model-checking in-lined reference monitors
- Gabow SCC
- Towards a notion of unsatisfiable and unrealizable cores for LTL
- scientific article; zbMATH DE number 1953030 (Why is no real title available?)
- scientific article; zbMATH DE number 2081113 (Why is no real title available?)
- scientific article; zbMATH DE number 1744956 (Why is no real title available?)
- scientific article; zbMATH DE number 1903371 (Why is no real title available?)
- scientific article; zbMATH DE number 1903378 (Why is no real title available?)
- Bounded semantics
- Automated verification of parallel nested DFS
- Farkas certificates and minimal witnesses for probabilistic reachability constraints
- Verified certification of reachability checking for timed automata
- Integrating topological proofs with model checking to instrument iterative design
- Proving the refuted: symbolic model checkers as proof generators
- Calculational design of a regular model checker by abstract interpretation
- Tools and Algorithms for the Construction and Analysis of Systems
- A theory of hints in model checking.
- Calculational design of a regular model checker by abstract interpretation
- On probability-raising causality in Markov decision processes
- Foundations of probability-raising causality in Markov decision processes
- Towards certified model checking for PLTL using one-pass tableaux
- \textsc{CoqCryptoLine}: a verified model checker with certified results
- Making \(\mathsf{IP}=\mathsf{PSPACE}\) practical: efficient interactive protocols for BDD algorithms
- A resolution-based interactive proof system for UNSAT
- Certifying rlive: a new proof strategy for liveness model checking
- A theorem prover based approach for SAT-based model checking certification
- Conflict-aware active automata learning
- Counterfactual causality for reachability and safety based on distance functions
- Certifying phase abstraction
- A resolution-based interactive proof system for UNSAT
- Progress in certifying hardware model checking results
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 Q4553254)
