WING 2010:Keyword Index

KeywordPapers
A
abstract interpretationAbstract Interpretation over Zones without Widening
accelerationTool Demonstration of the FLATA Counter Automata Toolset
automated reasoningSynthesising Functional Invariants in Separation Logic
C
concolic executionExtending Non-Termination Proof Techniques to Asynchronously Communicating Concurrent Programs
concurrent programsExtending Non-Termination Proof Techniques to Asynchronously Communicating Concurrent Programs
counter automataTool Demonstration of the FLATA Counter Automata Toolset
D
Discrete Event SystemsTropical linear programming and parametric mean payoff games
disjunctive domainsTropical linear programming and parametric mean payoff games
Disjunctive InvariantsLOOPUS - A Tool for Computing Loop Bounds for C Programs
F
finite model findersFinite countermodels as invariants. A case study in verification of parameterized mutual exclusion protocol
first-order predicate logicFinite countermodels as invariants. A case study in verification of parameterized mutual exclusion protocol
fixpoint equation systemsAbstract Interpretation over Zones without Widening
formal methodsFormal Requirements Capturing using VRS system
functional invariantsSynthesising Functional Invariants in Separation Logic
I
infinite-state systemsFinite countermodels as invariants. A case study in verification of parameterized mutual exclusion protocol
interval analysisAbstract Interpretation over Zones without Widening
invariant generationAutomated Invariant Generation for the Verification of Real-Time Systems
Synthesising Functional Invariants in Separation Logic
L
loop boundsLOOPUS - A Tool for Computing Loop Bounds for C Programs
loop invariantsLoopfrog — loop summarization for static analysis
loop summarizationLoopfrog — loop summarization for static analysis
LoopfrogLoopfrog — loop summarization for static analysis
M
mean-payoff gamesTropical linear programming and parametric mean payoff games
model checkingCheAPS: a Checker of Asynchronous Parameterized Systems
Formal Requirements Capturing using VRS system
N
non-terminationExtending Non-Termination Proof Techniques to Asynchronously Communicating Concurrent Programs
P
parameterizedCheAPS: a Checker of Asynchronous Parameterized Systems
parameterized systemsFinite countermodels as invariants. A case study in verification of parameterized mutual exclusion protocol
policy iterationTropical linear programming and parametric mean payoff games
program analysisLOOPUS - A Tool for Computing Loop Bounds for C Programs
program derivationCocktail II
program verificationAutomated Invariant Generation for the Verification of Real-Time Systems
R
reachabilityTool Demonstration of the FLATA Counter Automata Toolset
real-time systemsAutomated Invariant Generation for the Verification of Real-Time Systems
Requirements VerificationFormal Requirements Capturing using VRS system
S
separation logicSynthesising Functional Invariants in Separation Logic
specificationCocktail II
static analysisTropical linear programming and parametric mean payoff games
Loopfrog — loop summarization for static analysis
static program analysisAbstract Interpretation over Zones without Widening
Strategy Improvement AlgorithmsAbstract Interpretation over Zones without Widening
T
terminationExtending Non-Termination Proof Techniques to Asynchronously Communicating Concurrent Programs
LOOPUS - A Tool for Computing Loop Bounds for C Programs
theorem provingCocktail II
Extending Non-Termination Proof Techniques to Asynchronously Communicating Concurrent Programs
Formal Requirements Capturing using VRS system
timed automataAbstract Interpretation over Zones without Widening
toolCheAPS: a Checker of Asynchronous Parameterized Systems
transitive closureLOOPUS - A Tool for Computing Loop Bounds for C Programs
tropical algebraTropical linear programming and parametric mean payoff games
V
verificationAbstract Interpretation over Zones without Widening
CheAPS: a Checker of Asynchronous Parameterized Systems
Z
ZonesAbstract Interpretation over Zones without Widening