Journal: Formal Methods in System Design

Volume 47, Issue 3

265 -- 286Tarek Mhamdi, Osman Hasan, Sofiène Tahar. Evaluation of anonymity and confidentiality protocols using theorem proving
287 -- 301Sagar Chaki, Arie Gurfinkel, Ofer Strichman. Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation)
302 -- 360Eric Goubault, Sylvie Putot. A zonotopic framework for functional abstractions

Volume 47, Issue 2

159 -- 203Jonathan Heinen, Christina Jansen, Joost-Pieter Katoen, Thomas Noll. Juggrnaut: using graph grammars for abstracting unbounded heap structures
204 -- 229Dima Elenbogen, Shmuel Katz, Ofer Strichman. Proving mutual termination
230 -- 264Krishnendu Chatterjee, Martin Chmelik, Przemyslaw Daca. CEGAR for compositional analysis of qualitative properties in Markov decision processes

Volume 47, Issue 1

1 -- 25Philipp Rümmer, Hossein Hojjat, Viktor Kuncak. On recursion-free Horn clauses and Craig interpolation
26 -- 50Christian von Essen, Barbara Jobstmann. Program repair without regret
51 -- 74Yakir Vizel, Alexander Nadel, Vadim Ryvchin. Efficient generation of small interpolants in CNF
75 -- 92Daniel Kroening, Matt Lewis, Georg Weissenbacher. Under-approximating loops in C programs for fast counterexample detection
93 -- 119Loris D'Antoni, Margus Veanes. Extended symbolic finite automata and transducers
120 -- 157Pranav Garg 0001, Christof Löding, P. Madhusudan, Daniel Neider. Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists