EasyChair Publications
WING 2010 Volume Information
Volume:Andrei Voronkov, Laura Kovacs and Nikolaj Bjorner (editors)
WING 2010. Workshop on Invariant Generation 2010

WING 2010 Volume Information

Title:WING 2010. Workshop on Invariant Generation 2010
Editors:Andrei Voronkov, Laura Kovacs and Nikolaj Bjorner
Series:EPiC Series in Computing
Publication date:June 22, 2012


Leonardo de Moura and Nikolaj BjornerApplications and Challenges in Satisfiability Modulo Theories1-11
Thomas Martin Gawlitza and Helmut SeidlAbstract Interpretation over Zones without Widening12-43
Bahareh Badban, Stefan Leue and Jan-Georg SmausAutomated Invariant Generation for the Verification of Real-Time Systems44-58
Jan Olaf Blech, Thanh-Hung Nguyen and Michael PerinInvariants and Robustness of BIP Models59-74
Marius Bozga, Radu Iosif, Filip Konecny and Tomas VojnarTool Demonstration of the FLATA Counter Automata Toolset75
Florin Craciun, Chenguang Luo, Guanhua He, Shengchao Qin and Wei-Ngan ChinDiscovering Specifications for Unknown Procedures - Work in Progress76-91
Michael FranssenCocktail II92-93
Stephane Gaubert, Ricardo D. Katz and Sergei SergeevTropical linear programming and parametric mean payoff games94-110
Gudmund Grov and Andrew IrelandTowards Automated Property Discovery within Hume111-127
Igor KonnovCheAPS: a Checker of Asynchronous Parameterized Systems128-129
Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich and Christoph M. WintersteigerLoopfrog — loop summarization for static analysis130-131
Matthias Kuntz, Stefan Leue and Christoph SchebenExtending Non-Termination Proof Techniques to Asynchronously Communicating Concurrent Programs132-147
Alexander Letichevsky, Alexander Kolchin, Oleksandr Letychevskyi, Stepan Potiyenko, Vlad Volkov and Thomas WeigertFormal Requirements Capturing using VRS system148-149
Alexei LisitsaFinite countermodels as invariants. A case study in verification of parameterized mutual exclusion protocol150-151
Asma Louhichi, Olfa Mraihi, Lamia Labed Jilani and Ali MiliA Comparative Study of Invariant Assertions, Invariant Relations, and Invariant Functions152-166
Ewen Maclean, Andrew Ireland, Lucas Dixon and Robert AtkeyRefinement and Term Synthesis in Loop Invariant Generation167-182
Ewen Maclean, Andrew Ireland and Gudmund GrovSynthesising Functional Invariants in Separation Logic183-184
Moritz Sinn and Florian ZulegerLOOPUS - A Tool for Computing Loop Bounds for C Programs185-186
Angela WallenburgGeneralisation of Induction Formulae based on Proving by Symbolic Execution187-203


3theorem proving
2invariant generation, model checking, static analysis, termination, verification
1abstract interpretation, acceleration, automated reasoning, concolic execution, concurrent programs, counter automata, discrete event systems, disjunctive domains, disjunctive invariants, finite model finders, first order predicate logic, fixpoint equation systems, formal methods, functional invariants, infinite state systems, interval analysis, loop bounds, loop invariants, loop summarization, loopfrog, mean payoff games, non termination, parameterized, parameterized systems, policy iteration, program analysis, program derivation, program verification, reachability, real time systems, requirements verification, separation logic, specification, static program analysis, strategy improvement algorithms, timed automata, tool, transitive closure, tropical algebra, zones