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