| a |
| abstract interpretation | Abstract Interpretation over Zones without Widening |
| acceleration | Tool Demonstration of the FLATA Counter Automata Toolset |
| automated reasoning | Synthesising Functional Invariants in Separation Logic |
| c |
| concolic execution | Extending Non-Termination Proof Techniques to Asynchronously Communicating Concurrent Programs |
| concurrent programs | Extending Non-Termination Proof Techniques to Asynchronously Communicating Concurrent Programs |
| counter automata | Tool Demonstration of the FLATA Counter Automata Toolset |
| d |
| Discrete Event Systems | Tropical linear programming and parametric mean payoff games |
| disjunctive domains | Tropical linear programming and parametric mean payoff games |
| Disjunctive Invariants | LOOPUS - A Tool for Computing Loop Bounds for C Programs |
| f |
| finite model finders | Finite countermodels as invariants. A case study in verification of parameterized mutual exclusion protocol |
| first-order predicate logic | Finite countermodels as invariants. A case study in verification of parameterized mutual exclusion protocol |
| fixpoint equation systems | Abstract Interpretation over Zones without Widening |
| formal methods | Formal Requirements Capturing using VRS system |
| functional invariants | Synthesising Functional Invariants in Separation Logic |
| i |
| infinite-state systems | Finite countermodels as invariants. A case study in verification of parameterized mutual exclusion protocol |
| interval analysis | Abstract Interpretation over Zones without Widening |
| invariant generation | Automated Invariant Generation for the Verification of Real-Time Systems
Synthesising Functional Invariants in Separation Logic |
| l |
| loop bounds | LOOPUS - A Tool for Computing Loop Bounds for C Programs |
| loop invariants | Loopfrog — loop summarization for static analysis |
| loop summarization | Loopfrog — loop summarization for static analysis |
| Loopfrog | Loopfrog — loop summarization for static analysis |
| m |
| mean-payoff games | Tropical linear programming and parametric mean payoff games |
| model checking | CheAPS: a Checker of Asynchronous Parameterized Systems
Formal Requirements Capturing using VRS system |
| n |
| non-termination | Extending Non-Termination Proof Techniques to Asynchronously Communicating Concurrent Programs |
| p |
| parameterized | CheAPS: a Checker of Asynchronous Parameterized Systems |
| parameterized systems | Finite countermodels as invariants. A case study in verification of parameterized mutual exclusion protocol |
| policy iteration | Tropical linear programming and parametric mean payoff games |
| program analysis | LOOPUS - A Tool for Computing Loop Bounds for C Programs |
| program derivation | Cocktail II |
| program verification | Automated Invariant Generation for the Verification of Real-Time Systems |
| r |
| reachability | Tool Demonstration of the FLATA Counter Automata Toolset |
| real-time systems | Automated Invariant Generation for the Verification of Real-Time Systems |
| Requirements Verification | Formal Requirements Capturing using VRS system |
| s |
| separation logic | Synthesising Functional Invariants in Separation Logic |
| specification | Cocktail II |
| static analysis | Tropical linear programming and parametric mean payoff games
Loopfrog — loop summarization for static analysis |
| static program analysis | Abstract Interpretation over Zones without Widening |
| Strategy Improvement Algorithms | Abstract Interpretation over Zones without Widening |
| t |
| termination | Extending Non-Termination Proof Techniques to Asynchronously Communicating Concurrent Programs
LOOPUS - A Tool for Computing Loop Bounds for C Programs |
| theorem proving | Cocktail II
Extending Non-Termination Proof Techniques to Asynchronously Communicating Concurrent Programs
Formal Requirements Capturing using VRS system |
| timed automata | Abstract Interpretation over Zones without Widening |
| tool | CheAPS: a Checker of Asynchronous Parameterized Systems |
| transitive closure | LOOPUS - A Tool for Computing Loop Bounds for C Programs |
| tropical algebra | Tropical linear programming and parametric mean payoff games |
| v |
| verification | Abstract Interpretation over Zones without Widening
CheAPS: a Checker of Asynchronous Parameterized Systems |
| z |
| Zones | Abstract Interpretation over Zones without Widening |
