@inproceedings{Ballarin:2006:ILI:2079677.2079683,
 author = {Ballarin, Clemens},
 title = {Interpretation of Locales in Isabelle: Theories and Proof Contexts},
 booktitle = {Proceedings of the 5th International Conference on Mathematical Knowledge Management},
 series = {MKM'06},
 year = {2006},
 isbn = {3-540-37104-4, 978-3-540-37104-5},
 location = {Wokingham, UK},
 pages = {31--43},
 numpages = {13},
 acmid = {2079683},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg}
}

@article{DBLP:journals/jar/Ballarin14, 
 author = {Clemens Ballarin}, 
 title = {{L}ocales: {A} {M}odule {S}ystem for {M}athematical {T}heories}, 
 journal = {J. Autom. Reasoning}, 
 volume = {52}, 
 number = {2}, 
 pages = {123--153}, 
 year = {2014} 
}

@Article{HOL1,
  Title                    = {{A}n {I}ntroduction to {M}athematical {L}ogic and {T}ype {T}heory: to {T}ruth through {P}roof},
  Author                   = {Peter B.Andrews},
  Journal                  = {Kluwer Academic Publishers},
  Year                     = {1986},
  Owner                    = {yakoub},
  Timestamp                = {2015.05.26}
}

@article{DBLP:journals/sttt/BeyerHJM07,
  author    = {Dirk Beyer and
               Thomas A. Henzinger and
               Ranjit Jhala and
               Rupak Majumdar},
  title     = {{T}he {S}oftware {M}odel {C}hecker {B}last},
  journal   = {{STTT}},
  volume    = {9},
  number    = {5-6},
  pages     = {505--525},
  year      = {2007},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DBLP:conf/tacas/ClarkeKSY05,
  author    = {Edmund M. Clarke and
               Daniel Kroening and
               Natasha Sharygina and
               Karen Yorav},
  title     = {{SATABS:} {SAT}-{B}ased {P}redicate {A}bstraction for {ANSI-C}},
  booktitle = {Proceedings of {TACAS} '05},
  pages     = {570--574},
  year      = {2005},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@Article{Denise2011,
author="Denise, Alain
and Gaudel, Marie-Claude
and Gouraud, Sandrine-Dominique
and Lassaigne, Richard
and Oudinet, Johan
and Peyronnet, Sylvain",
title="{C}overage-biased {R}andom {E}xploration of large {M}odels and {A}pplication to {T}esting",
journal="International Journal on Software Tools for Technology Transfer",
year="2011",
volume="14",
number="1",
pages="73--93",
abstract="This paper presents several randomised algorithms for generating paths in large models according to a given coverage criterion. Using methods for counting combinatorial structures, these algorithms can efficiently explore very large models, based on a graphical representation by an automaton or by a product of several automata. This new approach can be applied to random exploration in order to optimise path coverage and can be generalised to take into account other coverage criteria, via the definition of a notion of randomised coverage satisfaction. Our main contributions are a method for drawing paths uniformly at random in composed models, i.e. models that are given as products of automata, first without and then with synchronisation; a new efficient approach to draw paths at random taking into account some other coverage criterion. Experimental results show promising agreement with theoretical predictions and significant improvement over previous randomised approaches. This work opens new perspectives for future studies of statistical testing and model checking, mainly to fight the combinatorial explosion problem.",
issn="1433-2787"
}

@inproceedings{DBLP:conf/pldi/GrebenshchikovLPR12,
  author    = {Sergey Grebenshchikov and
               Nuno P. Lopes and
               Corneliu Popeea and
               Andrey Rybalchenko},
  title     = {Synthesizing {S}oftware {V}erifiers from {P}roof {R}ules},
  booktitle = {Proceedings of {PLDI} '12},
  pages     = {405--416},
  year      = {2012},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DBLP:conf/cav/IvancicYGGSA05,
  author    = {Franjo Ivancic and
               Zijiang Yang and
               Malay K. Ganai and
               Aarti Gupta and
               Ilya Shlyakhter and
               Pranav Ashar},
  title     = {{F}-{S}oft: {S}oftware {V}erification {P}latform},
  booktitle = {Proceedings of {CAV} '05},
  pages     = {301--306},
  year      = {2005},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DBLP:conf/cav/JaffarMNS12,
  author    = {Joxan Jaffar and
               Vijayaraghavan Murali and
               Jorge A. Navas and
               Andrew E. Santosa},
  title     = {{TRACER:} {A} {S}ymbolic {E}xecution {T}ool for {V}erification},
  booktitle = {Proceedings of {CAV} '12},
  pages     = {758--766},
  year      = {2012},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{Jaffar:2011:USE:2341616.2341659,
 author = {Jaffar, Joxan and Navas, Jorge A. and Santosa, Andrew E.},
 title = {{U}nbounded {S}ymbolic {E}xecution for {P}rogram {V}erification},
 booktitle = {Proceedings of RV '11},
 year = {2012},
 pages = {396--411},
 acmid = {2341659},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
} 

@Inbook{McMillan2006,
author="McMillan, Kenneth L.",
editor="Ball, Thomas
and Jones, Robert B.",
chapter="Lazy Abstraction with Interpolants",
title="Proceedings of {CAV} '06",
year="2006",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="123--136"
}

@Book{nipkow.ea:isabelle:2002,
  Title                    = {{I}sabelle/{HOL}---{A} {P}roof {A}ssistant for {H}igher-{O}rder {L}ogic},
  Author                   = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  Publisher                = pub-springer,
  Year                     = {2002},

  Myaddress                  = pub-springer:adr,
  Series                   = s-lncs,
  Volume                   = {2283},

  Abstract                 = {This book is a self-contained introduction to interactive proof in higher-order logic (HOL), using the proof assistant Isabelle2002. It is a tutorial for potential users rather than a monograph for researchers. The book has three parts.
 1. Elementary Techniques shows how to model functional programs in higher-order logic. Early examples involve lists and the natural numbers. Most proofs are two steps long, consisting of induction on a chosen variable followed by the auto tactic. But even this elementary part covers such advanced topics as nested and mutual recursion. 2. Logic and Sets presents a collection of lower-level tactics that you can use to apply rules selectively. It also describes Isabelle/HOL's treatment of sets, functions and relations and explains how to define sets inductively. One of the examples concerns the theory of model checking, and another is drawn from a classic textbook on formal languages. 3. Advanced Material describes a variety of other topics. Among these are the real numbers, records and overloading. Advanced techniques are described involving induction and recursion. A whole chapter is devoted to an extended example: the verification of a security protocol.},
  Owner                    = {l-nemouchi},
  Timestamp                = {2014.03.20}
}

@Article{Noschinski2015,
author="Noschinski, Lars",
title="{A} {G}raph {L}ibrary for {I}sabelle",
journal="Mathematics in Computer Science",
year="2015",
volume="9",
number="1",
pages="23--39",
abstract="In contrast to other areas of mathematics such as calculus, number theory or probability theory, there is currently no standard library for graph theory for the Isabelle/HOL proof assistant. We present a formalization of directed graphs and essential related concepts. The library supports general infinite directed graphs (digraphs) with labeled and parallel arcs, but care has been taken not to complicate reasoning on more restricted classes of digraphs. We use this library to formalize a characterization of Euler Digraphs and to verify a method of checking Kuratowski subgraphs used in the LEDA library.",
issn="1661-8289",
doi="10.1007/s11786-014-0183-z",
url="https://doi.org/10.1007/s11786-014-0183-z"
}

@TECHREPORT{AGVW2016,
  AUTHOR =  {Aissat, R. and Gaudel, M.-C. and Voisin, F. and Wolff, B.},
  TITLE =         {Pruning Infeasible Paths via Graph Transformations and
Symbolic Execution: a Method and a Tool},
  NUMBER =        {1588},
  INSTITUTION =   {L.R.I., Univ. Paris-Sud},
  url = {https://www.lri.fr/srubrique.php?news=33},
  YEAR  =         {2016},
}

@inproceedings{AissatVW2016,
  Title                    = {Infeasible Paths Elimination by Symbolic Execution Techniques: Proof of Correctness and Preservation of Paths},
  Author                   = {Aissat, R. and Voisin, F. and Wolff, B.},
 booktitle = {{ITP'16}},
 Year = {2016},
   series    = {LNCS},
  volume    = {9807},
 location = {Vienna},
}

@article{brucker.ea:extensible:2008,
  author = {Achim D. Brucker and Burkhart Wolff},
  journal = {Journal of Automated Reasoning (JAR)},
  classification = {journal},
  language = {USenglish},
  note = {Serge Autexier, Heiko Mantel, Stephan Merz, and Tobias Nipkow (eds)},
  pdf = {https://www.lri.fr/~wolff/papers/journals/brucker.ea-extensible-2008-b.pdf},
  title = {{A}n {E}xtensible {E}ncoding of {O}bject-oriented {D}ata {M}odels in {HOL} with an {A}pplication to {IMP++}},
  volume = {Selected Papers of the AVOCS-VERIFY Workshop 2006},
  doi = {10.1007/s10817-008-9108-3},
  pages = {219-249},
  volume = 41,
  number = {3--4},
  year = 2008
}


@article{DBLP:journals/fac/Nipkow98,
  author    = {Tobias Nipkow},
  title     = {Winskel is (almost) Right: Towards a Mechanized Semantics},
  journal   = {Formal Asp. Comput.},
  volume    = {10},
  number    = {2},
  pages     = {171--186},
  year      = {1998},
  url       = {https://doi.org/10.1007/s001650050009},
  doi       = {10.1007/s001650050009}
}

@inproceedings{Oheimb:2002:HLN:647541.730154,
 author = {Oheimb, David von and Nipkow, Tobias},
 title = {Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited},
 series    = {LNCS},
 year = {2002},
 isbn = {3-540-43928-5},
 pages = {89--105},
 numpages = {17},
 url = {http://dl.acm.org/citation.cfm?id=647541.730154},
 acmid = {730154},
 publisher = {Springer-Verlag},
 keywords = {Isabelle/HOL, auxiliary variables, dynamic binding, hoare logic, java, side effects},
} 


@inproceedings{DBLP:conf/esop/Lochbihler12,
  author    = {Andreas Lochbihler},
  title     = {Java and the Java Memory Model - {A} Unified, Machine-Checked Formalisation},
  booktitle = {Programming Languages and Systems - 21st European Symposium on Programming,
               {ESOP} 2012, Held as Part of the European Joint Conferences on Theory
               and Practice of Software, {ETAPS} 2012, Tallinn, Estonia, March 24
               - April 1, 2012. Proceedings},
  pages     = {497--517},
  series    = {LNCS},
  publisher = {Springer-Verlag},
  year      = {2012},
  url       = {https://doi.org/10.1007/978-3-642-28869-2_25},
  doi       = {10.1007/978-3-642-28869-2_25}
}

