Volume •Abstracts •Preface •Authors •Keywords •BibTex Entries

WING 2010: Volume Information

WING 2010. Workshop on Invariant Generation 2010

Editors: Andrei Voronkov, Laura Kovacs and Nikolaj Bjorner

EPiC Series in Computing•Volume 1

19 articles•203 pages•Published: June 22, 2012

Papers

Applications and Challenges in Satisfiability Modulo Theories

Leonardo De Moura and Nikolaj Bjorner

1-11

Abstract Interpretation over Zones without Widening

Thomas Martin Gawlitza and Helmut Seidl

12-43

Automated Invariant Generation for the Verification of Real-Time Systems

Bahareh Badban, Stefan Leue and Jan-Georg Smaus

44-58

Invariants and Robustness of BIP Models

Jan Olaf Blech, Thanh-Hung Nguyen and Michael Perin

59-74

Tool Demonstration of the FLATA Counter Automata Toolset

Marius Bozga, Radu Iosif, Filip Konecny and Tomas Vojnar

75

Discovering Specifications for Unknown Procedures - Work in Progress

Florian Craciun, Chenguang Luo, Guanhua He, Shengchao Qin and Wei-Ngan Chin

76-91

Michael Franssen

92-93

Tropical linear programming and parametric mean payoff games

Stephane Gaubert, Ricardo Katz and Sergei Sergeev

94-110

Towards Automated Property Discovery within Hume

Gudmund Grov and Andrew Ireland

111-127

CheAPS: a Checker of Asynchronous Parameterized Systems

128-129

Loopfrog — loop summarization for static analysis

Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich and Christoph M. Wintersteiger

130-131

Extending Non-Termination Proof Techniques to Asynchronously Communicating Concurrent Programs

Matthias Kuntz, Stefan Leue and Christoph Scheben

132-147

Formal Requirements Capturing using VRS system

Alexander Letichevsky, Alexander Kolchin, Oleksandr Letychevskyy jr., Stepan Potiyenko, Vlad Volkov and Thomas Weigert

148-149

Finite countermodels as invariants. A case study in verification of parameterized mutual exclusion protocol

150-151

A Comparative Study of Invariant Assertions, Invariant Relations, and Invariant Functions

Asma Louhichi, Olfa Mraihi, Lamia Labed Jilani and Ali Mili

152-166

Refinement and Term Synthesis in Loop Invariant Generation

Ewen Maclean, Andrew Ireland, Lucas Dixon and Robert Atkey

167-182

Synthesising Functional Invariants in Separation Logic

Ewen Maclean, Andrew Ireland and Gudmund Grov

183-184

LOOPUS - A Tool for Computing Loop Bounds for C Programs

Moritz Sinn and Florian Zuleger

185-186

Generalisation of Induction Formulae based on Proving by Symbolic Execution

Angela Wallenburg

187-203

Keyphrases

abstract 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, invariant generation², loop bounds, loop invariants, loop summarization, Loopfrog, mean-payoff games, model checking², non-termination, parameterized, parameterized systems, policy iteration, program analysis, program derivation, program verification, reachability, real-time systems, Requirements Verification, separation logic, specification, static analysis², static program analysis, Strategy Improvement Algorithms, termination², theorem proving³, timed automata, tool, transitive closure, tropical algebra, verification², Zones.