642 papers · page 9 of 33
Quentin Bouillaguet, François Bobot, Mihaela Sighireanu, Boris Yakobowski
Cooperation between verification methods is crucial to tackle the challenging problem of software verification. The paper focuses on the verification of C programs using pointers and it formalizes a cooperation between static analyzers doing pointer analysis and a deductive verif…
Rémy Boutonnet, Nicolas Halbwachs
Abstract elided by the publisher.
Denis Bueno, Karem A. Sakallah
Abstract elided by the publisher.
Normann Decker, Anton Pirogov
This paper presents an approximation approach to verifying counter systems with respect to properties formulated in an expressive counting extension of linear temporal logic. It can express, e.g., that the number of acknowledgements never exceeds the number of requests to a servi…
Grigory Fedyukovich, Arie Gurfinkel, Aarti Gupta
Abstract elided by the publisher.
Gereon Fox, Daniel Stan, Holger Hermanns
Abstract elided by the publisher.
Hongfei Fu, Krishnendu Chatterjee
Abstract elided by the publisher.
Kimball Germane, Jay McCarthy, Michael D. Adams, Matthew Might
Abstract elided by the publisher.
Kimball Germane, Matthew Might
Abstract elided by the publisher.
Stefan Haar, Juraj Kolcák, Loïc Paulevé
Parametric models abstract part of the specification of dynamical models by integral parameters. They are for example used in computational systems biology, notably with parametric regulatory networks, which specify the global architecture (interactions) of the networks, while pa…
Jad Hamza, Viktor Kuncak
We study the problem of synthesizing string to string transformations from a set of input/output examples. The transformations we consider are expressed using deterministic finite automata (DFA) that read pairs of letters, one letter from the input and one from the output. The DF…
Jochen Hoenicke, Tanja Schindler
Abstract elided by the publisher.
Richard Huybers, Alfons Laarman
Abstract elided by the publisher.
Anja F. Karl, Robert Schilling, Roderick Bloem, Stefan Mangard
Abstract elided by the publisher.
Nuno P. Lopes, Andrey Rybalchenko
Abstract elided by the publisher.
Tianhan Lu, Pavol Cerný, Bor-Yuh Evan Chang, Ashutosh Trivedi
Our aim is to statically verify that in a given reactive program, the length of collection variables does not grow beyond a given bound. We propose a scalable type-based technique that checks that each collection variable has a given refinement type that specifies constraints abo…
Charlie Murphy, Zachary Kincaid
Abstract elided by the publisher.
Thanh-Toan Nguyen, Quang-Trung Ta, Wei-Ngan Chin
Abstract elided by the publisher.
Jens Nicolay, Quentin Stiévenart, Wolfgang De Meuter, Coen De Roover
Abstract elided by the publisher.
Viorel Preoteasa, Iulia Dragomir, Stavros Tripakis
Abstract elided by the publisher.