Cited in
(39)- Sound verification procedures for temporal properties of infinite-state systems
- Synchronizing the asynchronous
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- A decidable and expressive fragment of many-sorted first-order linear temporal logic
- scientific article; zbMATH DE number 7215283 (Why is no real title available?)
- Bounded quantifier instantiation for checking inductive invariants
- IMITATOR
- RESTART
- TLAPS
- TLC
- Ivy
- Mcmt
- MODIST
- Cubicle
- VeriCon
- PSync
- nuXmv
- ByMC
- Chapar
- DynamoDB
- Verdi
- FastTrack
- DiskPaxos
- GeoNames
- Scaling up livelock verification for network-on-chip routing algorithms
- Protocol combinators for modeling, testing, and execution of distributed systems
- dBug
- DCatch
- Koala
- IronFleet
- Temporal prophecy for proving temporal properties of infinite-state systems
- Learning inductive invariants by sampling from frequency distributions
- Certification of an exact worst-case self-stabilization time
- Sally
- Minha
- Btor2Tools
- \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
- SGGS decision procedures
- scientific article; zbMATH DE number 7533356 (Why is no real title available?)
This page was built for software: Ivy
