FAST
From MaRDI portal
FAST Q33078
Cited in
(56)- Automated Technology for Verification and Analysis
- Structural Presburger digit vector automata
- Verification and falsification of programs with loops using predicate abstraction
- Automatic verification of counter systems with ranking function
- Verification of qualitative \(\mathbb Z\) constraints
- Verification of flat FIFO systems
- Reachability in timed counter systems
- Forward analysis and model checking for trace bounded WSTS
- Experimenting Formal Proofs of Petri Nets Refinements
- Acceleration of the abstract fixpoint computation in numerical program analysis
- Applying abstract acceleration to (co-)reachability analysis of reactive programs
- \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
- Flat Petri nets (invited talk)
- How to Tackle Integer Weighted Automata Positivity
- The convex hull of a regular set of integer vectors is polyhedral and effectively computable
- Formal verification of real-time systems with preemptive scheduling
- Generalizing the template polyhedral domain
- Ehrenfeucht-Fraïssé goes automatic for real addition
- Some ways to reduce the space dimension in polyhedra computations
- scientific article; zbMATH DE number 7471708 (Why is no real title available?)
- Automatic Verification of Bossa Scheduler Properties
- Improving the results of program analysis by abstract interpretation beyond the decreasing sequence
- Verification of programs with half-duplex communication
- Verification of Flat FIFO Systems
- Expand, enlarge and check: new algorithms for the coverability problem of WSTS
- IMITATOR
- TREX
- PNML
- FLATA
- Aspic
- Dagger
- MONA
- PSync
- Antichains
- EUREKA
- LASH
- LIRA
- ByMC
- LoAT
- Reachability in parameterized systems: all flavors of threshold automata
- On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
- Don't care words with an application to the automata-based approach for real addition
- A calculus for modular loop acceleration
- Quadratic word equations with length constraints, counter systems, and Presburger arithmetic with divisibility
- Programs with lists are counter automata
- Symbolic model checking in non-Boolean domains
- The Power of Hybrid Acceleration
- Dense-choice counter machines revisited
- Quantitative separation logic and programs with lists
- Forward analysis and model checking for trace bounded WSTS
- Fair termination for parameterized probabilistic concurrent systems
- A case study on parametric verification of failure detectors
- Abstract fixpoint computations with numerical acceleration methods
- Extending abstract acceleration methods to data-flow programs with numerical inputs
- Guiding Craig interpolation with domain-specific abstractions
- Abstraction refinement and antichains for trace inclusion of infinite state systems
This page was built for software: FAST
