Document.bib

@InProceedings{Divine_3_0,
  author    = "Jiří Barnat and Luboš Brim and Vojtěch Havel
               and Jan Havlíček and Jan Kriho and Milan Lenčo
               and Petr Ročkai and Vladimír Štill and Jiří Weiser",
  title     = "{DiVinE 3.0 -- An Explicit-State Model Checker
                for Multithreaded C \& C++ Programs}",
  booktitle = "{Computer Aided Verification (CAV 2013)}",
  pages     = "863--868",
  volume    = "8044",
  series    = "LNCS",
  year      = "2013",
  publisher = "Springer"}

@inproceedings{Divine_LTL,
	location = {Norfolk, {VA}, United states},
	title = {Towards {LTL} model checking of unmodified thread-based C C++ programs},
	volume = {7226 {LNCS}},
	url = {http://dx.doi.org/10.1007/978-3-642-28891-3_25},
	abstract = {In this paper we present a new approach to verification of multi-threaded C/C++ programs. Our solution effectively chains the parallel and distributed-memory model checker {DiVinE} with {CLang} and the {LLVM} bitcode interpreter. This combination offers full {LTL}, distributed-memory model checking of virtually unmodified C/C++ source code and is supported by a newly introduced path-reduction technique. We demonstrate the efficiency of the reduction and also the capacity to produce human-readable counter-examples in two small case studies: a C implementation of the Peterson's mutual exclusion protocol and a C++ implementation of a shared-memory, lock-free {FIFO} data structure designed for fast inter-thread communication. \© 2012 Springer-Verlag.},
	pages = {252 -- 266},
	booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
	author = {Barnat, Jiri and Brim, Lubo and Rockai, Petr},
	date = {2012},
	keywords = {Data structures, Model checking, {NASA}},
}

@book{jiang_C_to_Promela,
	title = {Model Checking C Programs by Translating C to Promela},
	url = {http://www.diva-portal.org/smash/record.jsf?pid=diva2:235718},
	abstract = {Nowadays, the cost of program errors is increasing from day to day, so software reliability becomes a critical problem to the whole world. C is one of the most popular programming languages, and ha ...},
	author = {Jiang, Ke},
	urldate = {2017-02-06},
	date = {2009},
}

@article{SPIN,
  title={The model checker SPIN},
  author={Holzmann, Gerard J.},
  journal={IEEE Transactions on software engineering},
  volume={23},
  number={5},
  pages={279--295},
  year={1997},
  publisher={IEEE}
}

@inproceedings{Pancam,
	title = {Verifying Multi-threaded C Programs with {SPIN}},
	url = {http://link.springer.com/chapter/10.1007/978-3-540-85114-1_22},
	abstract = {A key challenge in model checking software is the difficulty of verifying properties of implementation code, as opposed to checking an abstract algorithmic description. We describe a tool for verifying multi-threaded C programs that uses the {SPIN} model checker. Our tool works by compiling a multi-threaded C program into a typed bytecode format, and then using a virtual machine that interprets the bytecode and computes new program states under the direction of {SPIN}. Our virtual machine is compatible with most of {SPIN}’s search options and optimization flags, such as bitstate hashing and multi-core checking. It provides support for dynamic memory allocation (the malloc and free family of functions), and for the pthread library, which provides primitives often used by multi-threaded C programs. A feature of our approach is that it can check code after compiler optimizations, which can sometimes introduce race conditions. We describe how our tool addresses the state space explosion problem by allowing users to define data abstraction functions and to constrain the number of allowed context switches. We also describe a reduction method that reduces context switches using dynamic knowledge computed on-the-fly, while being sound for both safety and liveness properties. Finally, we present initial experimental results with our tool on some small examples.},
	eventtitle = {International {SPIN} Workshop on Model Checking of Software},
	pages = {325--342},
	booktitle = {Model Checking Software},
	publisher = {Springer, Berlin, Heidelberg},
	author = {Zaks, Anna and Joshi, Rajeev},
	urldate = {2017-02-07},
	date = {2008-08-10},
	langid = {english},
	note = {{DOI}: 10.1007/978-3-540-85114-1\_22},
	keywords = {Abstracting, Codes (symbols), C (programming language), Microprocessor chips, Optimization, Probability density function, Program compilers, Spin dynamics, State space methods, Technical presentations},
}

@article{inspect,
  title={Runtime model checking of multithreaded C/C++ programs},
  author={Yang, Yu and Chen, Xiaofang and Gopalakrishnan, Ganesh and Kirby, Robert M},
  year={2007},
  publisher={Citeseer}
}

@article{CHESS,
	title = {{CHESS}: A systematic testing tool for concurrent software},
	url = {https://www.microsoft.com/en-us/research/publication/chess-a-systematic-testing-tool-for-concurrent-software/},
	shorttitle = {{CHESS}},
	abstract = {Concurrency is used pervasively in the development of large systems programs. However, concurrent programming is difficult because of the possibility of unexpected interference among concurrently executing tasks. Such interference often results in “Heisenbugs” that appear rarely and are extremely difficult to reproduce and debug. Stress testing, in which the system is run under heavy load …},
	journaltitle = {Microsoft Research},
	author = {Musuvathi, Madan and Qadeer, Shaz and Ball, Tom},
	urldate = {2017-02-02},
	date = {2007-11-01},
}

@inproceedings{CIVL,
	title = {{CIVL}: Formal Verification of Parallel Programs},
	doi = {10.1109/ASE.2015.99},
	shorttitle = {{CIVL}},
	abstract = {{CIVL} is a framework for static analysis and verification of concurrent programs. One of the main challenges to practical application of these techniques is the large number of ways to express concurrency: {MPI}, {OpenMP}, {CUDA}, and Pthreads, for example, are just a few of many "concurrency dialects" in wide use today. These dialects are constantly evolving and it is increasingly common to use several of them in a single "hybrid" program. {CIVL} addresses these problems by providing a concurrency intermediate verification language, {CIVL}-C, as well as translators that consume C programs using these dialects and produce {CIVL}-C. Analysis and verification tools which operate on {CIVL}-C can then be applied easily to a wide variety of concurrent C programs. We demonstrate {CIVL}'s error detection and verification capabilities on (1) an {MPI}+{OpenMP} program that estimates π and contains a subtle race condition, and (2) an {MPI}-based 1d-wave simulator that fails to conform to a simple sequential implementation.},
	eventtitle = {2015 30th {IEEE}/{ACM} International Conference on Automated Software Engineering ({ASE})},
	pages = {830--835},
	booktitle = {2015 30th {IEEE}/{ACM} International Conference on Automated Software Engineering ({ASE})},
	author = {Zheng, M. and Rogers, M. S. and Luo, Z. and Dwyer, M. B. and Siegel, S. F.},
	date = {2015-11},
}

@online{SARL,
  title = {{SARL}: The Symbolic Algebra Reasoning Library},
	url = {http://vsl.cis.udel.edu/sarl/},
	urldate = {2017-06-06},
}

@inproceedings{Impara,
	title = {Verifying multi-threaded software with impact},
	doi = {10.1109/FMCAD.2013.6679412},
	abstract = {Lazy abstraction with interpolants, also known as the Impact algorithm, is en vogue as a state-of-the-art software model-checking technique for sequential programs. However, a direct extension of the Impact algorithm to concurrent programs is bound to be inefficient as it has to explore all thread interleavings, which leads to control-state explosion. To this end, we present a new algorithm that combines a new, symbolic form of partial-order reduction with Impact. Our algorithm carries out the dependence analysis on-the-fly while constructing the abstraction and is thus able to deal precisely with dynamic dependencies arising from accesses to tables or pointers - a setting where classical static partial-order reduction techniques struggle. We have implemented the algorithm in a prototype tool that analyses concurrent C program with {POSIX} threads and evaluated it on a number of benchmark programs. To our knowledge, this is the first application of an Impact-like algorithm to concurrent programs.},
	eventtitle = {2013 Formal Methods in Computer-Aided Design},
	pages = {210--217},
	booktitle = {2013 Formal Methods in Computer-Aided Design},
	author = {Wachter, B. and Kroening, D. and Ouaknine, J.},
	date = {2013-10},
}

@inproceedings{IMPACT,
	title = {Lazy Abstraction with Interpolants},
	url = {http://link.springer.com/chapter/10.1007/11817963_14},
	abstract = {We describe a model checker for infinite-state sequential programs, based on Craig interpolation and the lazy abstraction paradigm. On device driver benchmarks, we observe a speedup of up to two orders of magnitude relative to a similar tool using predicate abstraction.},
	eventtitle = {International Conference on Computer Aided Verification},
	pages = {123--136},
	booktitle = {Computer Aided Verification},
	publisher = {Springer, Berlin, Heidelberg},
	author = {{McMillan}, Kenneth L.},
	urldate = {2017-02-06},
	date = {2006-08-17},
	langid = {english},
	note = {{DOI}: 10.1007/11817963\_14},
}

@inproceedings{Satabs,
	location = {Tallinn, Estonia},
	title = {{SatAbs}: A bit-precise verifier for C programs (competition contribution)},
	volume = {7214 {LNCS}},
	url = {http://dx.doi.org/10.1007/978-3-642-28756-5_47},
	abstract = {{SatAbs} is a bit-precise software model checker for {ANSI}-C programs. It implements sound predicate-abstraction based algorithms for both sequential and concurrent software. \© 2012 Springer-Verlag Berlin Heidelberg.},
	pages = {552 -- 555},
	booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
	author = {Basler, Gerard and Donaldson, Alastair and Kaiser, Alexander and Kroening, Daniel and Tautschnig, Michael and Wahl, Thomas},
	date = {2012},
	keywords = {C (programming language), Model checking}
}

@article{clarkesatabs,
  title={SATABS: SAT-based Predicate Abstraction for ANSI-C},
  author={Clarke, Edmund and Kroening, Daniel and Sharygina, Natasha and Yorav, Karen}
}


@inproceedings{Threader_theory,
	location = {New York, {NY}, {USA}},
	title = {Predicate Abstraction and Refinement for Verifying Multi-threaded Programs},
	isbn = {978-1-4503-0490-0},
	url = {http://doi.acm.org/10.1145/1926385.1926424},
	doi = {10.1145/1926385.1926424},
	series = {{POPL} '11},
	abstract = {Automated verification of multi-threaded programs requires explicit identification of the interplay between interacting threads, so-called environment transitions, to enable scalable, compositional reasoning. Once the environment transitions are identified, we can prove program properties by considering each program thread in isolation, as the environment transitions keep track of the interleaving with other threads. Finding adequate environment transitions that are sufficiently precise to yield conclusive results and yet do not overwhelm the verifier with unnecessary details about the interleaving with other threads is a major challenge. In this paper we propose a method for safety verification of multi-threaded programs that applies (transition) predicate abstraction-based discovery of environment transitions, exposing a minimal amount of information about the thread interleaving. The crux of our method is an abstraction refinement procedure that uses recursion-free Horn clauses to declaratively state abstraction refinement queries. Then, the queries are resolved by a corresponding constraint solving algorithm. We present preliminary experimental results for mutual exclusion protocols and multi-threaded device drivers.},
	pages = {331--344},
	booktitle = {Proceedings of the 38th Annual {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages},
	publisher = {{ACM}},
	author = {Gupta, Ashutosh and Popeea, Corneliu and Rybalchenko, Andrey},
	urldate = {2017-02-09},
	date = {2011},
}

@inproceedings{Threader,
	location = {Rome, Italy},
	title = {Threader: A verifier for multi-threaded programs: (Competition contribution)},
	volume = {7795 {LNCS}},
	url = {http://dx.doi.org/10.1007/978-3-642-36742-7_51},
	abstract = {Threader is a tool that automates verification of safety and termination properties for multi-threaded C programs. The distinguishing feature of Threader is its use of reasoning that is compositional with regards to the thread structure of the verified program. This paper describes the verification approach taken by Threader and provides instructions on how to install and use the tool. \© 2013 Springer-Verlag.},
	pages = {633 -- 636},
	booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
	author = {Popeea, Corneliu and Rybalchenko, Andrey},
	date = {2013},
	keywords = {Artificial intelligence},
}

@inproceedings{CPAChecker,
  title={CPAchecker: A tool for configurable software verification},
  author={Beyer, Dirk and Keremoglu, M Erkan},
  booktitle={International Conference on Computer Aided Verification},
  pages={184--190},
  year={2011},
  organization={Springer}
}

@article{CPAChecker_multithread,
  title={A Light-Weight Approach for Verifying Multi-Threaded Programs with CPAchecker},
  author={Beyer, Dirk and Friedberger, Karlheinz},
  journal={arXiv preprint arXiv:1612.04983},
  year={2016}
}

@inproceedings{CBMC,
	title = {A Tool for Checking {ANSI}-C Programs},
	url = {http://link.springer.com/chapter/10.1007/978-3-540-24730-2_15},
	abstract = {We present a tool for the formal verification of {ANSI}-C programs using Bounded Model Checking ({BMC}). The emphasis is on usability: the tool supports almost all {ANSI}-C language features, including pointer constructs, dynamic memory allocation, recursion, and the float and double data types. From the perspective of the user, the verification is highly automated: the only input required is the {BMC} bound. The tool is integrated into a graphical user interface. This is essential for presenting long counterexample traces: the tool allows stepping through the trace in the same way a debugger allows stepping through a program.},
	eventtitle = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
	pages = {168--176},
	booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
	publisher = {Springer, Berlin, Heidelberg},
	author = {Clarke, Edmund and Kroening, Daniel and Lerda, Flavio},
	urldate = {2017-02-07},
	date = {2004-03-29},
	langid = {english},
	note = {{DOI}: 10.1007/978-3-540-24730-2\_15},
}


@inproceedings{ESBMC_k_induction,
	location = {Rome, Italy},
	title = {Handling unbounded loops with {ESBMC} 1.20: (Competition contribution)},
	volume = {7795 {LNCS}},
	url = {http://dx.doi.org/10.1007/978-3-642-36742-7_47},
	abstract = {We extended {ESBMC} to exploit the combination of context-bounded symbolic model checking and k-induction to prove safety properties in single- and multi-threaded {ANSI}-C programs with unbounded loops. We now first try to verify by induction that the safety property holds in the system. If that fails, we search for a bounded reachable state that constitutes a counterexample. \© 2013 Springer-Verlag.},
	pages = {619 -- 622},
	booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
	author = {Morse, Jeremy and Cordeiro, Lucas and Nicole, Denis and Fischer, Bernd},
	date = {2013},
	keywords = {Model checking},
}

@inproceedings{ESBMC,
	location = {Tallinn, Estonia},
	title = {Context-bounded model checking with {ESBMC} 1.17 (competition contribution)},
	volume = {7214 {LNCS}},
	url = {http://dx.doi.org/10.1007/978-3-642-28756-5_42},
	abstract = {{ESBMC} is a context-bounded symbolic model checker for single- and multi-threaded {ANSI}-C code. It converts the verification conditions using different background theories and passes them directly to an {SMT} solver. \© 2012 Springer-Verlag Berlin Heidelberg.},
	pages = {534 -- 537},
	booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
	author = {Cordeiro, Lucas and Morse, Jeremy and Nicole, Denis and Fischer, Bernd},
	date = {2012},
	keywords = {Algorithms, C (programming language)},
}

@inproceedings{CSeq,
	location = {Palo Alto, {CA}, United states},
	title = {{CSeq}: A concurrency pre-processor for sequential C verification tools},
	url = {http://dx.doi.org/10.1109/ASE.2013.6693139},
	abstract = {Sequentialization translates concurrent programs into equivalent nondeterministic sequential programs so that the different concurrent schedules no longer need to be handled explicitly. It can thus be used as a concurrency preprocessing technique for automated sequential program verification tools. Our {CSeq} tool implements a novel sequentialization for C programs using pthreads, which extends the Lal/Reps sequentialization to support dynamic thread creation. {CSeq} now works with three different backend tools, {CBMC}, {ESBMC}, and {LLBMC}, and is competitive with state-of-the-art verification tools for concurrent programs. \© 2013 {IEEE}.},
	pages = {710 -- 713},
	booktitle = {2013 28th {IEEE}/{ACM} International Conference on Automated Software Engineering, {ASE} 2013 - Proceedings},
	author = {Fischer, Bernd and Inverso, Omar and Parlato, Gennaro},
	date = {2013},
	keywords = {Automation, Software engineering},
}

@inproceedings{LazyCSeq,
	title = {Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization},
	url = {http://link.springer.com/chapter/10.1007/978-3-319-08867-9_39},
	series = {Lecture Notes in Computer Science},
	abstract = {Bounded model checking ({BMC}) has successfully been used for many practical program verification problems, but concurrency still poses a challenge. Here we describe a new approach to {BMC} of sequentially consistent C programs using {POSIX} threads. Our approach first translates a multi-threaded C program into a nondeterministic sequential C program that preserves reachability for all round-robin schedules with a given bound on the number of rounds. It then re-uses existing high-performance {BMC} tools as backends for the sequential verification problem. Our translation is carefully designed to introduce very small memory overheads and very few sources of nondeterminism, so that it produces tight {SAT}/{SMT} formulae, and is thus very effective in practice: our prototype won the concurrency category of {SV}-{COMP}14. It solved all verification tasks successfully and was 30x faster than the best tool with native concurrency handling.},
	eventtitle = {International Conference on Computer Aided Verification},
	pages = {585--602},
	booktitle = {Computer Aided Verification},
	publisher = {Springer International Publishing},
	author = {Inverso, Omar and Tomasco, Ermenegildo and Fischer, Bernd and Torre, Salvatore La and Parlato, Gennaro},
	editor = {Biere, Armin and Bloem, Roderick},
	urldate = {2017-02-06},
	date = {2014-07-18},
	langid = {english},
	note = {{DOI}: 10.1007/978-3-319-08867-9\_39},
}

@inproceedings{MuCSeq,
	title = {Verifying Concurrent Programs by Memory Unwinding},
	url = {https://link.springer.com/chapter/10.1007/978-3-662-46681-0_52},
	doi = {10.1007/978-3-662-46681-0_52},
	abstract = {We describe a new sequentialization-based approach to the symbolic verification of multithreaded programs with shared memory and dynamic thread creation. Its main novelty is the idea of memory unwinding ({MU}), i.e., a sequence of write operations into the shared memory. For the verification, we nondeterministically guess an {MU} and then simulate the behavior of the program according to any scheduling that respects it. This approach is complementary to other sequentializations and explores an orthogonal dimension, i.e., the number of write operations. It also simplifies the implementation of several important optimizations, in particular the targeted exposure of individual writes. We implemented this approach as a code-to-code transformation from multithreaded into nondeterministic sequential programs, which allows the reuse of sequential verification tools. Experiments show that our approach is effective: it found all errors in the concurrency category of {SV}-{COMP}15.},
	eventtitle = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
	pages = {551--565},
	booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
	publisher = {Springer, Berlin, Heidelberg},
	author = {Tomasco, Ermenegildo and Inverso, Omar and Fischer, Bernd and Torre, Salvatore La and Parlato, Gennaro},
	urldate = {2017-03-09},
	date = {2015-04-11},
	langid = {english},
}

@inproceedings{ULCSeq,
	location = {Chiba, Japan},
	title = {Lazy sequentialization for the safety verification of unbounded concurrent programs},
	volume = {9938 {LNCS}},
	url = {http://dx.doi.org/10.1007/978-3-319-46520-3_12},
	abstract = {Lazy sequentialization has emerged as one of the most promising approaches for concurrent program analysis but the only efficient implementation given so far works just for bounded programs. This restricts the approach to bug-finding purposes. In this paper, we describe and evaluate a new lazy sequentialization translation that does not unwind loops and thus allows to analyze unbounded computations, even with an unbounded number of context switches. In connection with an appropriate sequential backend verification tool it can thus also be used for the safety verification of concurrent programs, rather than just for bug-finding. The main technical novelty of our translation is the simulation of the thread resumption in a way that does not use gotos and thus does not require that each statement is executed at most once. We have implemented this translation in the {UL}-{CSeq} tool for C99 programs that use the pthreads {API}.We evaluate {UL}-{CSeq} on several benchmarks, using different sequential verification backends on the sequentialized program, and show that it is more effective than previous approaches in proving the correctness of the safe benchmarks, and still remains competitive with state-of-the-art approaches for finding bugs in the unsafe benchmarks. \© Springer International Publishing {AG} 2016.},
	pages = {174 -- 191},
	booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
	author = {Nguyen, Truc L. and Fischer, Bernd and La Torre, Salvatore and Parlato, Gennaro},
	date = {2016},
	keywords = {Program debugging},
}

@article{BLAST,
  title={The software model checker Blast},
  author={Beyer, Dirk and Henzinger, Thomas A and Jhala, Ranjit and Majumdar, Rupak},
  journal={International Journal on Software Tools for Technology Transfer},
  volume={9},
  number={5-6},
  pages={505--525},
  year={2007},
  publisher={Springer}
}

@inproceedings{predicate_abstraction_over_approximation,
	title = {Over-Approximating Boolean Programs with Unbounded Thread Creation},
	doi = {10.1109/FMCAD.2006.24},
	abstract = {This paper describes a symbolic algorithm for over-approximating reachability in Boolean programs with unbounded thread creation. The fix-point is detected by projecting the state of the threads to the globally visible parts, which are finite. Our algorithm models recursion by over-approximating the call stack that contains the return locations of recursive function calls, as reachability is undecidable in this case. The algorithm may obtain spurious counterexamples, which are removed iteratively by means of an abstraction refinement loop. Experiments show that the symbolic algorithm for unbounded thread creation scales to large abstract models},
	eventtitle = {2006 Formal Methods in Computer Aided Design},
	pages = {53--59},
	booktitle = {2006 Formal Methods in Computer Aided Design},
	author = {Cook, B. and Kroening, D. and Sharygina, N.},
	date = {2006-11},
}

@inproceedings{thread_modular_abstraction,
	title = {Thread-Modular Abstraction Refinement},
	url = {https://link.springer.com/chapter/10.1007/978-3-540-45069-6_27},
	doi = {10.1007/978-3-540-45069-6_27},
	abstract = {We present an algorithm called Tar (“Thread-modular Abstraction Refinement”) for model checking safety properties of concurrent software. The Tar algorithm uses thread-modular assume-guarantee reasoning to overcome the exponential complexity in the control state of multithreaded programs. Thread modularity means that Tar explores the state space of one thread at a time, making assumptions about how the environment can interfere. The Tar algorithm uses counterexample-guided predicate-abstraction refinement to overcome the usually infinite complexity in the data state of C programs. A successive approximation scheme automatically infers the necessary precision on data variables as well as suitable environment assumptions. The scheme is novel in that transition relations are approximated from above, while at the same time environment assumptions are approximated from below. In our software verification tool Blast we have implemented a fully automatic race checker for multithreaded C programs which is based on the Tar algorithm. This tool has verified a wide variety of commonly used locking idioms, including locking schemes that are not amenable to existing dynamic and static race checkers such as Eraser or Warlock.},
	eventtitle = {International Conference on Computer Aided Verification},
	pages = {262--274},
	booktitle = {Computer Aided Verification},
	publisher = {Springer, Berlin, Heidelberg},
	author = {Henzinger, Thomas A. and Jhala, Ranjit and Majumdar, Rupak and Qadeer, Shaz},
	urldate = {2017-06-12},
	date = {2003-07-08},
	langid = {english},
}

@inproceedings{svcomp_2017_result,
  title={Software Verification with Validation of Results},
  author={Dirk Beyer},
  booktitle={International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  pages={331--349},
  year={2017},
  organization={Springer}
}

@inproceedings{svcomp_2016_result,
  title={Reliable and reproducible competition results with benchexec and witnesses (report on SV-COMP 2016)},
  author={Dirk Beyer},
  booktitle={International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  pages={887--904},
  year={2016},
  organization={Springer}
}

@inproceedings{svcomp_2015_result,
  title={Software Verification and Verifiable Witnesses},
  author={Dirk Beyer},
  booktitle={Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems-Volume 9035},
  pages={401--416},
  year={2015},
  organization={Springer-Verlag New York, Inc.}
}

@inproceedings{svcomp_2014_result,
    author = {Dirk Beyer},
    title = {Status Report on Software Verification - (Competition Summary SV-COMP 2014)},
    booktitle = {In Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
    year = {2014},
    pages = {373--388}
}

@online{LTL_scheme,
	title = {Property Pattern Mappings for {LTL}},
	url = {http://patterns.projects.cs.ksu.edu/documentation/patterns/ltl.shtml},
	urldate = {2017-04-05},
}

@inproceedings{ltl2ba,
	title = {Fast {LTL} to Büchi Automata Translation},
	url = {https://link.springer.com/chapter/10.1007/3-540-44585-4_6},
	doi = {10.1007/3-540-44585-4_6},
	abstract = {We present an algorithm to generate Büchi automata from {LTL} formulae. This algorithm generates a very weak alternating co-Büchi automaton and then transforms it into a Büchi automaton, using a generalized Büchi automaton as an intermediate step. Each automaton is simplified on-the-fly in order to save memory and time. As usual we simplify the {LTL} formula before any treatment. We implemented this algorithm and compared it with Spin: the experiments show that our algorithm is much more efficient than Spin. The criteria of comparison are the size of the resulting automaton, the time of the computation and the memory used. Our implementation is available on the web at the following address: http://verif.liafa.jussieu.fr/ltl2ba},
	eventtitle = {International Conference on Computer Aided Verification},
	pages = {53--65},
	booktitle = {Computer Aided Verification},
	publisher = {Springer, Berlin, Heidelberg},
	author = {Gastin, Paul and Oddoux, Denis},
	urldate = {2017-05-01},
	date = {2001-07-18},
	langid = {english},
	file = {ltl2ba.md:/home/nephe/Documents/Research/notes/ltl2ba.md:text/markdown;Snapshot:/home/nephe/.mozilla/firefox/ayqx710h.default-1473031361475/zotero/storage/PPGWATBE/3-540-44585-4_6.html:text/html}
}

@Article{morse_ltl,
author="Morse, Jeremy
and Cordeiro, Lucas
and Nicole, Denis
and Fischer, Bernd",
title="Model checking LTL properties over ANSI-C programs with bounded traces",
journal="Software {\&} Systems Modeling",
year="2015",
month="02",
day="01",
volume="14",
number="1",
pages="65--81",
abstract="Context-bounded model checking has been used successfully to verify safety properties in multi-threaded systems automatically, even if they are implemented in low-level programming languages such as C. In this paper, we describe and experiment with an approach to extend context-bounded software model checking to safety and liveness properties expressed in linear-time temporal logic (LTL). Our approach checks the actual C program, rather than an extracted abstract model. It converts the LTL formulas into B{\"u}chi automata for the corresponding never claims and then further into C monitor threads that are interleaved with the execution of the program under analysis. This combined system is then checked using the ESBMC model checker. We use an extended, four-valued LTL semantics to handle the finite traces that bounded model checking explores; we thus check the combined system several times with different acceptance criteria to derive the correct truth value. In order to mitigate the state space explosion, we use a dedicated scheduler that selects the monitor thread only after updates to global variables occurring in the LTL formula. We demonstrate our approach on the analysis of the sequential firmware of a medical device and a small multi-threaded control application.",
issn="1619-1374",
doi="10.1007/s10270-013-0366-0",
url="https://doi.org/10.1007/s10270-013-0366-0"
}


@book{25_years_of_model_checking,
  title={25 years of model checking: history, achievements, perspectives},
  author={Grumberg, Orna and Veith, Helmut},
  volume={5000},
  year={2008},
  publisher={Springer}
	isbn = {978-3-540-69849-4 978-3-540-69850-0},
	url = {http://link.springer.com/10.1007/978-3-540-69850-0},
	note = {{DOI}: 10.1007/978-3-540-69850-0}
}

@manual{ocamlrefman,
  author = {Xavier Leroy
  and Damien Doligez
  and Alain Frisch
  and Jacques Garrigue
  and Didier R\'emy
  and J\'er\^ome Vouillon},
  title = {The OCaml system (release 4.04): Documentation and user's manual},
  organization = {Institut National de Recherche en Informatique et en Automatique},
  year = 2016,
  month = nov,
  url = {http://caml.inria.fr/distrib/ocaml-3.12/ocaml-3.12-refman.pdf},
}

@article{ocamlgraph,
  title={Designing a Generic Graph Library Using ML Functors.},
  author={Conchon, Sylvain and Filli{\^a}tre, Jean-Christophe and Signoles, Julien},
  journal={Trends in functional programming},
  volume={8},
  pages={124--140},
  year={2007}
}

@online{json,
	title = {{JSON}},
	url = {http://www.json.org/},
	urldate = {2017-08-29},
}

@Inbook{cil,
author="Necula, George C.
and McPeak, Scott
and Rahul, Shree P.
and Weimer, Westley",
editor="Horspool, R. Nigel",
title="CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs",
bookTitle="Compiler Construction: 11th International Conference, CC 2002 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8--12, 2002 Proceedings",
year="2002",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="213--228",
abstract="This paper describes the C Intermediate Language: a highlevel representation along with a set of tools that permit easy analysis and source-to-source transformation of C programs.",
isbn="978-3-540-45937-8",
doi="10.1007/3-540-45937-5_16",
url="https://doi.org/10.1007/3-540-45937-5_16"
}

@article{mtl_definition,
  title={Specifying real-time properties with metric temporal logic},
  author={Koymans, Ron},
  journal={Real-time systems},
  volume={2},
  number={4},
  pages={255--299},
  year={1990},
  publisher={Springer}
}
@article{OBDD,
 author = {Bryant, Randal E.},
 title = {Graph-Based Algorithms for Boolean Function Manipulation},
 journal = {IEEE Trans. Comput.},
 issue_date = {August 1986},
 volume = {35},
 number = {8},
 month = aug,
 year = {1986},
 issn = {0018-9340},
 pages = {677--691},
 numpages = {15},
 url = {http://dx.doi.org/10.1109/TC.1986.1676819},
 doi = {10.1109/TC.1986.1676819},
 acmid = {6433},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
 keywords = {Boolean functions, binary decision diagrams, logic design verification, symbolic manipulation, symbolic manipulation, Boolean functions, binary decision diagrams, logic design verification},
}

@article{dsilva_survey_2008,
	title = {A Survey of Automated Techniques for Formal Software Verification},
	volume = {27},
	issn = {0278-0070},
	doi = {10.1109/TCAD.2008.923410},
	abstract = {The quality and the correctness of software are often the greatest concern in electronic systems. Formal verification tools can provide a guarantee that a design is free of specific flaws. This paper surveys algorithms that perform automatic static analysis of software to detect programming errors or prove their absence. The three techniques considered are static analysis with abstract domains, model checking, and bounded model checking. A short tutorial on these techniques is provided, highlighting their differences when applied to practical problems. This paper also surveys tools implementing these techniques and describes their merits and shortcomings.},
	pages = {1165--1178},
	number = {7},
	journaltitle = {{IEEE} Transactions on Computer-Aided Design of Integrated Circuits and Systems},
	author = {D'Silva, V. and Kroening, D. and Weissenbacher, G.},
	date = {2008-07},
}


@inproceedings{ESBMC_multithread,
	location = {Waikiki, Honolulu, {HI}, United states},
	title = {Verifying multi-threaded software using {SMT}-based context-bounded model checking},
	rights = {Compendex},
	url = {http://dx.doi.org/10.1145/1985793.1985839},
	abstract = {We describe and evaluate three approaches to model check multi-threaded software with shared variables and locks using bounded model checking based on Satisfiability Modulo Theories ({SMT}) and our modelling of the synchronization primitives of the Pthread library. In the lazy approach, we generate all possible interleavings and call the {SMT} solver on each of them individually, until we either find a bug, or have systematically explored all interleavings. In the schedule recording approach, we encode all possible interleavings into one single formula and then exploit the high speed of the {SMT} solvers. In the underapproximation and widening approach, we reduce the state space by abstracting the number of interleavings from the proofs of unsatisfiability generated by the {SMT} solvers. In all three approaches, we bound the number of context switches allowed among threads in order to reduce the number of interleavings explored. We implemented these approaches in {ESBMC}, our {SMT}-based bounded model checker for {ANSI}-C programs. Our experiments show that {ESBMC} can analyze larger problems and substantially reduce the verification time compared to state-of-the-art techniques that use iterative context-bounding algorithms or counter-example guided abstraction refinement. \© 2011 {ACM}.},
	pages = {331 -- 340},
	booktitle = {Proceedings - International Conference on Software Engineering},
	author = {Cordeiro, Lucas and Fischer, Bernd},
	date = {2011},
}

@inproceedings{SymDivine,
	location = {Eindhoven, Netherlands},
	title = {{SymDIVINE}: Tool for Control-Explicit Data-Symbolic state space exploration},
	volume = {9641},
	rights = {Compendex},
	url = {http://dx.doi.org/10.1007/978-3-319-32582-8_14},
	abstract = {We present {SymDIVINE}: a tool for bit-precise model checking of parallel C and C++ programs. It builds upon {LLVM} compiler infrastructure, hence, it uses {LLVM} {IR} as an input formalism. Internally, {SymDIVINE} extends the standard explicit-state state space exploration with {SMT} machinery to handle non-deterministic data values. As such, {SymDIVINE} is on a halfway between a symbolic executor and an explicitstate model checker. The key differentiating aspect present in {SymDIVINE} is the ability to decide about equality of two symbolically represented states preventing thus repeated exploration of the state space graph. This is crucially important in particular for verification of parallel programs where the state space graph is full of diamond-shaped subgraphs. \© Springer International Publishing Switzerland 2016.},
	pages = {208 -- 213},
	booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
	author = {Mrazek, Jan and Bauch, Petr and Lauko, Henrich and Barnat, Jii},
	date = {2016},
}

@online{assertion_regehr,
	title = {Use of Assertions – Embedded in Academia},
	url = {https://blog.regehr.org/archives/1091},
	titleaddon = {Embedded in Academia},
	author = {Regehr, John},
	urldate = {2017-10-12},
}

@inproceedings{abstract_state_graph,
	title = {Construction of abstract state graphs with {PVS}},
	isbn = {978-3-540-63166-8 978-3-540-69195-2},
	url = {https://link.springer.com/chapter/10.1007/3-540-63166-6_10},
	doi = {10.1007/3-540-63166-6_10},
	series = {Lecture Notes in Computer Science},
	abstract = {In this paper, we propose a method for the automatic construction of an abstract state graph of an arbitrary system using the Pvs theorem prover.Given a parallel composition of sequential processes and a partition of the state space induced by predicates ϕ1, ..., g4l on the program variables which defines an abstract state space, we construct an abstract state graph, starting in the abstract initial state. The possible successors of a state are computed using the Pvs theorem prover by verifying for each index i if ϕi or ¬ϕi is a postcondition of it. This allows an abstract state space exploration for arbitrary programs.},
	eventtitle = {International Conference on Computer Aided Verification},
	pages = {72--83},
	booktitle = {Computer Aided Verification},
	publisher = {Springer, Berlin, Heidelberg},
	author = {Graf, Susanne and Saidi, Hassen},
	urldate = {2017-10-11},
	date = {1997-06-22},
	langid = {english},
}

@online{horror_story,
	title = {Software Horror Stories},
	url = {https://www.cs.tau.ac.il/~nachumd/horror.html},
	titleaddon = {{SOFTWARE} {HORROR} {STORIES}},
	author = {Dershowitz, Nachum},
	urldate = {2017-03-30},
}

@inproceedings{pnueli_LTL,
	title = {The temporal logic of programs},
	doi = {10.1109/SFCS.1977.32},
	abstract = {A unified approach to program verification is suggested, which applies to both sequential and parallel programs. The main proof method suggested is that of temporal reasoning in which the time dependence of events is the basic concept. Two formal systems are presented for providing a basis for temporal reasoning. One forms a formalization of the method of intermittent assertions, while the other is an adaptation of the tense logic system Kb, and is particularly suitable for reasoning about concurrent programs.},
	eventtitle = {18th Annual Symposium on Foundations of Computer Science (sfcs 1977)},
	pages = {46--57},
	booktitle = {18th Annual Symposium on Foundations of Computer Science (sfcs 1977)},
	author = {Pnueli, A.},
	date = {1977-10},
}

@inproceedings{RCTL_formulas,
	location = {London, {UK}, {UK}},
	title = {On-the-Fly Model Checking of {RCTL} Formulas},
	isbn = {978-3-540-64608-2},
	url = {http://dl.acm.org/citation.cfm?id=647767.733619},
	series = {{CAV} '98},
	pages = {184--194},
	booktitle = {Proceedings of the 10th International Conference on Computer Aided Verification},
	publisher = {Springer-Verlag},
	author = {Beer, Ilan and Ben-David, Shoham and Landver, Avner},
	urldate = {2017-11-01},
	date = {1998}
}


@article{Rust,
 author = {Matsakis, Nicholas D. and Klock,II, Felix S.},
 title = {The Rust Language},
 journal = {Ada Lett.},
 issue_date = {December 2014},
 volume = {34},
 number = {3},
 month = oct,
 year = {2014},
 issn = {1094-3641},
 pages = {103--104},
 numpages = {2},
 url = {http://doi.acm.org/10.1145/2692956.2663188},
 doi = {10.1145/2692956.2663188},
 acmid = {2663188},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@inproceedings{SMACK,
  title={SMACK software verification toolchain},
  author={Carter, Montgomery and He, Shaobo and Whitaker, Jonathan and Rakamari{\'c}, Zvonimir and Emmi, Michael},
  booktitle={Proceedings of the 38th International Conference on Software Engineering Companion},
  pages={589--592},
  year={2016},
  organization={ACM}
}

@incollection{SKINK,
	location = {Berlin, Heidelberg},
	title = {Skink: Static Analysis of Programs in {LLVM} Intermediate Representation},
	volume = {10206},
	isbn = {978-3-662-54579-9 978-3-662-54580-5},
	url = {http://link.springer.com/10.1007/978-3-662-54580-5_27},
	shorttitle = {Skink},
	pages = {380--384},
	booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
	publisher = {Springer Berlin Heidelberg},
	author = {Cassez, Franck and Sloane, Anthony M. and Roberts, Matthew and Pigram, Matthew and Suvanpong, Pongsak and de Aledo, Pablo Gonzalez},
	editor = {Legay, Axel and Margaria, Tiziana},
	urldate = {2017-11-21},
	date = {2017},
	note = {{DOI}: 10.1007/978-3-662-54580-5\_27}
}

@online{SQLite_test,
	title = {How {SQLite} Is Tested},
	url = {https://www.sqlite.org/testing.html},
	urldate = {2017-11-22},
}


@article{CHESS,
	title = {{CHESS}: A systematic testing tool for concurrent software},
	url = {https://www.microsoft.com/en-us/research/publication/chess-a-systematic-testing-tool-for-concurrent-software/},
	shorttitle = {{CHESS}},
	journaltitle = {Microsoft Research},
	author = {Musuvathi, Madan and Qadeer, Shaz and Ball, Tom},
	date = {2007-11-01},
}