CAVA LTL Modelchecker
From MaRDI portal
Cited in
(68)- CoSMed: a confidentiality-verified social media platform
- Formally verified algorithms for upper-bounding state space diameters
- Markov chains and Markov decision processes in Isabelle/HOL
- Refinement to imperative HOL
- JGraphT
- A graph library for Isabelle
- CoCon: a conference management system with formally verified document confidentiality
- Certifying proofs for SAT-based model checking
- CakeML
- TeMP
- From LCF to Isabelle/HOL
- Poly/ML
- From LTL to deterministic automata. A safraless compositional approach
- Automatic refinement to efficient data structures: a comparison of two approaches
- Locales
- Autoref
- Eisbach
- ConfiChair
- CFML
- libclang
- CoSMed: a confidentiality-verified social media platform
- Jif
- CoSMed
- Ur/Web
- Comprehending Isabelle/HOL’s Consistency
- ltl2dstar
- Fiat
- CAMPY
- GRAT
- InKreSAT
- Pfold
- Myhill-Nerode
- Edmonds-Karp
- Dijkstra Shortest Path
- Refinement Monadic
- Gauss-Jordan
- CAVA Automata Library
- CAVA
- Stuttering Equivalence
- Markov Models
- Perron Frobenius
- Collections
- NASA PVS
- LTL_to_DRA
- Tree Automata
- Gabow SCC
- Hotel Key Card
- Imperative Refinement
- LTL_to_GBA
- Real_Impl
- Hereditarily Finite Sets
- Finite Automata HF
- Knuth Morris Pratt
- JRIF
- Program-Conflict-Analysis
- IEEE_Floating_Point
- BDDTab
- AutoCorres
- Dune
- FlowFox
- Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
- Boolean_Expression_Checkers
- CoCon
- Efficient verified (UN)SAT certificate checking
- Pacheck
- Transition_Systems_and_Automata
- Formal verification of an executable LTL model checker with partial order reduction
- Optimising the ProB model checker for B using partial order reduction
This page was built for software: CAVA LTL Modelchecker
