@InProceedings{DBLP:conf/icalp/GrooteV90,
  author       = {Jan Friso Groote and Frits W. Vaandrager},
  title        = {An Efficient Algorithm for Branching Bisimulation
                  and Stuttering Equivalence},
  year         = 1990,
  booktitle    = {Proceedings of  the 17th
                  International Colloquium on Automata, Languages and Programming (ICALP 90)},
  address = {Warwick University, England, UK},
  pages        = {626--638},
  series    = {Lecture Notes in Computer Science},
  volume    = {443},
  publisher = {Springer},
}



@PhdThesis{klein13,
  author =       {Joachim Klein},
  title =        {Compositional Synthesis and Most General Controller},
  school =       {Technische Universit{\"a}t Dresden},
  year =         2013}

@InProceedings{MichaudD15,
  author       = {Thibaud Michaud and Alexandre Duret{-}Lutz},
  title        = {Practical Stutter-Invariance Checks for
                  {\(\omega\)}-Regular Languages},
  year         = 2015,
  booktitle    = {Proceedings of the 22nd International
                  Symposium on Model Checking Software (SPIN 2015)},
 address = {Stellenbosch, South Africa},
  pages        = {84--101},
  editor    = {Bernd Fischer and
               Jaco Geldenhuys},
  series    = {Lecture Notes in Computer Science},
  volume    = {9232},
  publisher = {Springer},
}



@inproceedings{lamport1983what,
  author = {Leslie Lamport},
  title = {What Good is Temporal Logic?},
  year = {1983},
  editor = {R. E. A. Mason},
  booktitle = {{IFIP} Congress on Information Processing},
  pages = {657--668},
}

@article{kuvcera2005stuttering,
  author = {Anton{\'{\i}}n Ku{\v{c}}era and Jan Strej{\v{c}}ek},
  title = {The stuttering principle revisited},
  year = {2005},
  volume = {41},
  number = {7--8},
  pages = {415--434},
  doi = {10.1007/s00236-005-0164-4},
  journal = {Acta Informatica},
}

@InProceedings{Clarkson2014,
  author       = {Michael R. Clarkson and Bernd Finkbeiner and Masoud
                  Koleini and Kristopher K. Micinski and Markus
                  N. Rabe and C{\'{e}}sar S{\'{a}}nchez},
  title        = {Temporal Logics for Hyperproperties},
  year         = 2014,
  booktitle    = {Proceedings of the Third International Conference on
                  Principles of Security and Trust ({POST} 2014)},
  address   =    {Grenoble, France},
  pages     = {265--284},
  editor    = {Mart{\'{\i}}n Abadi and
               Steve Kremer},
  series    = {Lecture Notes in Computer Science},
  volume    = {8414},
  publisher = {Springer},
}




@inproceedings{nguyenvan:hal-01583815,
	title = { A Symbolic Operational Semantics for {TESL} with an Application to Heterogeneous System Testing },
	author = { Nguyen Van, Hai and Balabonski, Thibaut and Boulanger, Fr{\'e}d{\'e}ric and Keller, Chantal and Valiron, Benoît and Wolff, Burkhart },
	booktitle = { Formal Modeling and Analysis of Timed Systems, 15th International Conference FORMATS 2017 },
	publisher = { Springer },
	series = { LNCS },
	volume = { 10419 },
	year = { 2017 },
	month = { Sep },
	date = { September 5-7 2017 },
	keywords = { Heterogeneity ; Synchronicity ; Timed Behaviors },
	pdf = { https://hal-centralesupelec.archives-ouvertes.fr/hal-01583815/file/article.pdf },
	hal_id = { hal-01583815 },
	hal_version = { v1 },
}
@book{Gordon:1993:IHT:155278,
 editor = {Gordon, M. J. C. and Melham, T. F.},
 title = {Introduction to {HOL}: A Theorem Proving Environment for Higher Order Logic},
 year = {1993},
 isbn = {0-521-44189-7},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
}

@INPROCEEDINGS{Eker03tamingheterogeneity,
    author = {Johan Eker and Jörn W. Janneck and Edward A. Lee and Jie Liu and Xiaojun Liu and Jozsef Ludvig and Stephen Neuendorffer and Sonia Sachs and Yuhong Xiong},
    title = {Taming Heterogeneity - The {Ptolemy} Approach},
    booktitle = {Proceedings of the IEEE},
    year = {2003},
    pages = {127--144}
}

@book{combemale:hal-01224096,
  TITLE = {Globalizing Domain-Specific Languages},
  AUTHOR = {Combemale, Benoit and Cheng, Betty H.C. and France, Robert B. and Jezequel, Jean-Marc and Rumpe, Bernhard},
  PDF = {http://www.springer.com/us/book/9783319261713},
  PUBLISHER = {{Springer International Publishing}},
  SERIES = {LNCS, Programming and Software Engineering},
  VOLUME = {9400},
  YEAR = {2015},
}

@inproceedings{varalarsen:hal-01182773,
  TITLE = {A Behavioral Coordination Operator Language {(BCOoL)}},
  AUTHOR = {Vara Larsen, Matias Ezequiel and Deantoni, Julien and Combemale, Benoit and Mallet, Fr{\'e}d{\'e}ric},
  booktitle = {{18th International Conference on Model Driven Engineering Languages and Systems (MODELS 2015)}},
  YEAR = {2015},
  MONTH = Aug,
  KEYWORDS = {Heterogeneous Modeling ; Coordination Languages ; DSMLs},
  PDF = {https://hal.inria.fr/hal-01182773/file/models2015-bcool.pdf},
  HAL_ID = {hal-01182773},
}

@inproceedings{garces:inria-00597981,
  TITLE = {A Model-Based Approach for Reconciliation of Polychronous Execution Traces},
  AUTHOR = {Garc{\'e}s, Kelly and Deantoni, Julien and Mallet, Fr{\'e}d{\'e}ric},
  BOOKTITLE = {{SEAA 2011 - 37th EUROMICRO Conference on Software Engineering and Advanced Applications}},
  ADDRESS = {Oulu, Finland},
  PUBLISHER = {{IEEE}},
  YEAR = {2011},
  MONTH = Aug,
  KEYWORDS = {Traces ; Logical time ; Debugging ; Verification ; Model-Driven Engineering},
  PDF = {https://hal.inria.fr/inria-00597981/file/garces_deantoni_mallet_SEAA2011.pdf},
  HAL_ID = {inria-00597981},
  HAL_VERSION = {v1},
}

@article
{2009MPMSimulation,
title = { Exploring Multi-Paradigm Modeling Techniques },
author = { C{\'e}cile Hardebolle and Fr{\'e}d{\'e}ric Boulanger },
journal = { SIMULATION: Transactions of The Society for Modeling and Simulation International },
volume = { 85 },
number = { 11/12 },
pages = { 688-708 },
year = { 2009 },
month = { November/December },
publisher = { SAGE Publications },
issn = { 0037-5497 },
impfact = { 0.404 (2007) },
rank = { B (CORE 2009) },
class = { intjournal },
}

@inproceedings{BouJacHarPro2014MEMOCODE,
title = {{TESL}: a Language for Reconciling Heterogeneous Execution Traces },
author = { Boulanger, Fr{\'e}d{\'e}ric and Jacquet, Christophe and Hardebolle, C{\'e}cile and Prodan, Iuliana },
language = { English },
affiliation = { Sup{\'e}lec Sciences des Syst{\`e}mes - EA4454 - E3S },
booktitle = { Twelfth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2014)},
pages = { 114-123 },
address = { Lausanne, Switzerland },
audience = { internationale },
year = { 2014 },
month = { Oct },
isbn = { 978-1-4799-5336-3 },
ieee = { CFP14MCD-USB },
pdf = { http://wdi.supelec.fr/boulanger/publis/2014MemoCODE.pdf },
class = { intconf },
}



@Manual{MARTE,
    key = {MARTE},
    title = {{UML} Profile for {MARTE}\texttrademark:  Modeling and Analysis of Real-time Embedded Systems},
  organization = {OMG -- Object Management Group},
  year =      2010,
}

@article{TSMLee98,
  author = 	 {Edward A. Lee and Alberto Sangiovanni-Vincentelli},
  title = 	 {A Framework for Comparing Models of Computation},
  journal =  {IEEE Trans. CAD},
  year = 	 {1998},
  volume = 	 {17},
  number = 	 {12},
}


@article{VIROLI200774,
title = "A core calculus for correlation in orchestration languages",
journal = "The Journal of Logic and Algebraic Programming",
volume = "70",
number = "1",
pages = "74 - 95",
year = "2007",
note = "",
issn = "1567-8326",
author = "Mirko Viroli",
keywords = "Web Services",
keywords = "Orchestration languages",
keywords = "Process algebras"
}

@misc{AndrewsBPEL2003,
  key = "BPEL",
  authors = "Tony Andrews et al.",
  title = "Specification: Business Process Execution Language for Web Services version 1.1",
  year = "2003",
}


@article{DBLP:journals/stp/Tretmans96,
  author    = {Jan Tretmans},
  title     = {Test Generation with Inputs, Outputs and Repetitive Quiescence},
  journal   = {Software - Concepts and Tools},
  volume    = {17},
  number    = {3},
  pages     = {103--120},
  year      = {1996},
  timestamp = {Thu, 03 Jan 2002 12:26:55 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/stp/Tretmans96},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@misc{onlinetestingsymposion,
  title = "International Online Testing Symposion",
  year = "1995-2017",
}


@Inbook{Schmaltz2008,
author="Schmaltz, Julien
and Tretmans, Jan",
editor="Cassez, Franck
and Jard, Claude",
title="On Conformance Testing for Timed Systems",
bookTitle="Formal Modeling and Analysis of Timed Systems: 6th International Conference, FORMATS 2008, Saint Malo, France, September 15-17, 2008. Proceedings",
year="2008",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="250--264",
isbn="978-3-540-85778-5",
}

@MISC{Berry96theconstructive,
    author = {G. Berry},
    title = {The Constructive Semantics of Pure {Esterel}},
    year = {1996},
    howpublished = {Draft}
}

@incollection{Berry:2000:FE:345868.345908,
 author = {Berry, G{\'e}rard},
 title = {The Foundations of {Esterel}},
 booktitle = {Proof, Language, and Interaction},
 editor = {Plotkin, Gordon and Stirling, Colin and Tofte, Mads},
 year = {2000},
 isbn = {0-262-16188-5},
 pages = {425--454},
 numpages = {30},
 acmid = {345908},
 publisher = {MIT Press},
 address = {Cambridge, MA, USA},
}

@article{mallet:inria-00371371,
year={2008},
issn={1614-5046},
journal={Innovations in Systems and Software Engineering},
volume={4},
number={3},
title={Clock constraint specification language: specifying clock constraints~with {UML/Marte}},
publisher={Springer-Verlag},
keywords={Unified modeling language; Time model; Constraints; MARTE},
author={Mallet, Fr{\'e}d{\'e}ric},
pages={309-314},
language={English}
}

@Inproceedings{Zhang2016,
author="Zhang, M.
and Mallet, F.",
title="An Executable Semantics of {Clock Constraint Specification Language} and Its Applications",
bookTitle="Formal Techniques for Safety-Critical Systems: 4th International Workshop, FTSCS 2015",
year="2016",
publisher="Springer",
address="Cham",
pages="37--51",
isbn="978-3-319-29510-7",
}

@article{mallet:inria-00464894,
  TITLE = {The {Clock Constraint Specification Language} for building timed causality models},
  AUTHOR = {Mallet, Fr{\'e}d{\'e}ric and Deantoni, Julien and Andr{\'e}, Charles and De Simone, Robert},
  JOURNAL = {{Innovations in Systems and Software Engineering}},
  PUBLISHER = {{Springer Verlag}},
  VOLUME = {6},
  NUMBER = {1-2},
  PAGES = {99-106},
  YEAR = {2010},
  MONTH = Mar,
  KEYWORDS = {CCSL ; SDF ; MoCC},
  HAL_ID = {inria-00464894},
  HAL_VERSION = {v1},
}

@Book{Nipkow-Paulson-Wenzel:2002,
  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  title		= {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
  publisher	= {Springer},
  series	= {LNCS},
  volume	= 2283,
  year		= 2002
}

@inproceedings{Weeks:2006:WCM:1159876.1159877,
 author = {Weeks, Stephen},
 title = {Whole-program {Compilation} in {MLton}},
 booktitle = {Proceedings of the 2006 Workshop on ML},
 series = {ML '06},
 year = {2006},
 isbn = {1-59593-483-9},
 location = {Portland, Oregon, USA},
 pages = {1--1},
 numpages = {1},
 acmid = {1159877},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@ARTICLE {
    vcd-954909, 
    journal={{IEEE} Std 1364-2001}, 
    title={{IEEE} Standard {Verilog} Hardware Description Language}, 
    year={2001}, 
}

@inproceedings{DBLP:conf/tap/BruckerW16,
  author    = {Achim D. Brucker and
               Burkhart Wolff},
  title     = {Monadic Sequence Testing and Explicit Test-Refinements},
  booktitle = {Tests and Proofs - 10th International Conference, {TAP} 2016, Held
               as Part of {STAF} 2016, Vienna, Austria, July 5-7, 2016, Proceedings},
  pages     = {17--36},
  year      = {2016},
  timestamp = {Wed, 22 Jun 2016 11:12:01 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/tap/BruckerW16},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}


@inproceedings{DBLP:conf/fm/TejW97,
  author    = {Haykal Tej and
               Burkhart Wolff},
  title     = {A Corrected Failure Divergence Model for {CSP} in {Isabelle/HOL}},
  booktitle = {{FME} '97: Industrial Applications and Strengthened Foundations of
               Formal Methods, 4th International Symposium of Formal Methods Europe,
               Graz, Austria, September 15-19, 1997, Proceedings},
  pages     = {318--337},
  year      = {1997},
  timestamp = {Thu, 15 Jun 2017 21:40:56 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/fm/TejW97},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{DBLP:journals/jar/BruckerW08,
  author    = {Achim D. Brucker and
               Burkhart Wolff},
  title     = {An Extensible Encoding of Object-oriented Data Models in {HOL}},
  journal   = {J. Autom. Reasoning},
  volume    = {41},
  number    = {3-4},
  pages     = {219--249},
  year      = {2008},
  timestamp = {Tue, 06 Jun 2017 22:17:53 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jar/BruckerW08},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{Krichen:2009:CTR:1541661.1541692,
 author = {Krichen, Moez and Tripakis, Stavros},
 title = {Conformance Testing for Real-time Systems},
 journal = {Form. Methods Syst. Des.},
 issue_date = {June      2009},
 volume = {34},
 number = {3},
 month = jun,
 year = {2009},
 issn = {0925-9856},
 pages = {238--304},
 numpages = {67},
 acmid = {1541692},
 publisher = {Kluwer Academic Publishers},
 address = {Hingham, MA, USA},
 keywords = {Conformance testing, Coverage, On-the-fly algorithms, Partial observability, Real-time systems, Specification and verification, Test generation, Timed automata},
}

@ARTICLE{lustre:ieee,
   AUTHOR={N. Halbwachs and P. Caspi and P. Raymond and D. Pilaud},
   TITLE={The synchronous dataflow programming language {Lustre}},
   JOURNAL={Proceedings of the IEEE},
   VOLUME={79},
   NUMBER={9},
   PAGES={1305-1320},
   MONTH={September},
   YEAR={1991}
}

@article{LEGUERNIC1987359,
title = "Synchronous Data Flow Programming with the Language {SIGNAL}",
journal = "IFAC Proceedings Volumes",
volume = "20",
number = "2",
pages = "359 - 364",
year = "1987",
note = "2nd IFAC Workshop on Adaptive Systems in Control and Signal Processing 1986, Lund, Sweden, 30 June-2 July 1986",
issn = "1474-6670",
author = "P. Le Guernic and A. Benveniste and P. Bournai and T. Gautier"
}

@inproceedings{talpin:hal-00763371,
  TITLE = {Constructive Polychronous Systems},
  AUTHOR = {Talpin, Jean-Pierre and Brandt, Jens and Gem{\"u}nde, Mike and Schneider, Klaus and Shukla, Sandeep},
  BOOKTITLE = {{Logical Foundations of Computer Science}},
  ADDRESS = {San Diego, CA, United States},
  EDITOR = {Artemov, Sergei and Nerode, Anil},
  PUBLISHER = {{Springer}},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {7734},
  YEAR = {2013},
  MONTH = Jan,
  PDF = {https://hal.inria.fr/hal-00763371/file/TBGS13.pdf},
  HAL_ID = {hal-00763371},
  HAL_VERSION = {v1},
}

@ARTICLE{Alur94atheory,
    author = {Rajeev Alur and David L. Dill},
    title = {A Theory of Timed Automata},
    journal = {Theoretical Computer Science},
    year = {1994},
    volume = {126},
    pages = {183--235}
}

@inproceedings{leguernic:hal-01240440,
  TITLE = {Polychronous Automata},
  AUTHOR = {Le Guernic, Paul and Gautier, Thierry and Talpin, Jean-Pierre and Besnard, Lo{\"i}c},
  BOOKTITLE = {{TASE 2015, 9th International Symposium on Theoretical Aspects of Software Engineering}},
  ADDRESS = {Nanjing, China},
  PUBLISHER = {{IEEE Computer Society}},
  PAGES = {95-102},
  YEAR = {2015},
  MONTH = Sep,
  PDF = {https://hal.archives-ouvertes.fr/hal-01240440/file/tase15.pdf},
  HAL_ID = {hal-01240440},
  HAL_VERSION = {v1},
}

@unpublished{montin:hal-01503384,
  TITLE = {{Clock Constraints Specification Langage} : A mechanized denotational semantics in {Agda}},
  AUTHOR = {Montin, Mathieu and Pantel, Marc},
  NOTE = {working paper or preprint},
  YEAR = {2017},
  MONTH = Apr,
  KEYWORDS = {CCSL ; Denotational semantics ; Proof assistant ; Agda},
  PDF = {https://hal.archives-ouvertes.fr/hal-01503384/file/tase_2017.pdf},
  HAL_ID = {hal-01503384},
  HAL_VERSION = {v1},
}

@techreport{deantoni:hal-01082274,
  TITLE = {{CCSL} denotational semantics},
  AUTHOR = {Deantoni, Julien and Andr{\'e}, Charles and Gascon, R{\'e}gis},
  TYPE = {Research Report},
  NUMBER = {RR-8628},
  PAGES = {29},
  INSTITUTION = {{Inria}},
  YEAR = {2014},
  MONTH = Nov,
  KEYWORDS = {CCSL ; MARTE ; denotational semantics ; timesquare ; polychronous},
  PDF = {https://hal.inria.fr/hal-01082274/file/RR-8628.pdf},
  HAL_ID = {hal-01082274},
  HAL_VERSION = {v1},
}

@InProceedings{Garnacho2013,
author="Garnacho, Manuel
and Bodeveix, Jean-Paul
and Filali-Amine, Mamoun",
editor="Braberman, V{\'i}ctor
and Fribourg, Laurent",
title="A Mechanized Semantic Framework for Real-Time Systems",
bookTitle="Formal Modeling and Analysis of Timed Systems: 11th International Conference, FORMATS 2013, Buenos Aires, Argentina, August 29-31, 2013. Proceedings",
year="2013",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="106--120",
abstract="Concurrent systems consist of many components which may execute in parallel and are complex to design, to analyze, to verify, and to implement. The complexity increases if the systems have real-time constraints, which are very useful in avionic, spatial and other kind of embedded applications. In this paper we present a logical framework for defining and validating real-time formalisms as well as reasoning methods over them. For this purpose, we have implemented in the Coq proof assistant well known semantic domains for real-time systems based on labelled transitions systems and timed runs. We experiment our framework by considering the real-time CSP-based language fiacre, which has been defined as a pivot formalism for modeling languages (aadl, sdl, ...) used in the TOPCASED project. Thus, we define an extension to the formal semantic models mentioned above that facilitates the modeling of fine-grained time constraints of fiacre. Finally, we implement this extension in our framework and provide a proof method environment to deal with real-time system in order to achieve their formal certification.",
isbn="978-3-642-40229-6",
}

@Inproceedings{Paulin-Mohring2001,
author="Paulin-Mohring, Christine",
editor="Kobayashi, Naoki
and Pierce, Benjamin C.",
title="Modelisation of Timed Automata in {Coq}",
bookTitle="Theoretical Aspects of Computer Software: 4th International Symposium, TACS 2001 Sendai, Japan, October 29--31, 2001 Proceedings",
year="2001",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="298--315",
abstract="This paper presents the modelisation of a special class of timed automata, named p-automata in the proof assistant Coq. This work was performed in the framework of the CALIFE project1 which aims to build a general platform for specification, validation and test of critical algorithms involved in telecommunications. This paper does not contain new theoretical results but explains how to combine and adapt known techniques in order to build an environment dedicated to a class of problems. It emphasizes the specific features of Coq which have been used, in particular dependent types and tactics based on computational reflection.",
isbn="978-3-540-45500-4",
}

@Article{Hale1993,
author="Hale, Roger
and Cardell-Oliver, Rachel
and Herbert, John",
title="An embedding of Timed Transition Systems in {HOL}",
journal="Formal Methods in System Design",
year="1993",
month="Aug",
day="01",
volume="3",
number="1",
pages="151--174",
abstract="The theory of Timed Transition Systems developed by Henzinger, Manna, and Pnueli provides a formal framework for specifying and reasoning about real-time systems. In this paper, we report on some preliminary investigations into the mechanization of this theory using the HOL theorem prover.",
issn="1572-8102",

}

@article{DBLP:journals/mscs/TripakisSSL13,
  author    = {Stavros Tripakis and
               Christos Stergiou and
               Chris Shaver and
               Edward A. Lee},
  title     = {A modular formal semantics for {Ptolemy}},
  journal   = {Mathematical Structures in Computer Science},
  volume    = {23},
  number    = {4},
  pages     = {834--881},
  year      = {2013},
  timestamp = {Thu, 08 Jun 2017 09:09:45 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/mscs/TripakisSSL13},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@TECHREPORT{scott-strachey,
  AUTHOR = {D. Scott and C. Strachey},
  TITLE = {Toward a Mathematical Semantics for Computer
                            Languages},
  TYPE = {Programming Research Group Technical 
                           Monograph},
  INSTITUTION = {Oxford Univ.\ Computing Lab.},
  YEAR = 1971
}

@InProceedings{10.1007/BFb0039592,
author="Kahn, G.",
title="Natural semantics",
booktitle="STACS 87",
year="1987",
publisher="Springer",
address="Berlin, Heidelberg",
pages="22--39",
abstract="During the past few years, many researchers have begun to present semantic specifications in a style that has been strongly advocated by Plotkin in [19]. The purpose of this paper is to introduce in an intuitive manner the essential ideas of the method that we call now Natural Semantics, together with its connections to ideas in logic and computing. Natural Semantics is of interest per se and because it is used as a semantics specification formalism for an interactive computer system that we are currently building at INRIA.",
isbn="978-3-540-47419-7"
}

@article{200417,
title = "A structural approach to operational semantics",
author = "G.~D. Plotkin",
journal = "The Journal of Logic and Algebraic Programming",
volume = "60-61",
pages = "17 - 139",
year = "2004",
note = "Structural Operational Semantics",
issn = "1567-8326",
}

@book{Nipkow:2014:CSI:2717090,
 author = {Nipkow, Tobias and Klein, Gerwin},
 title = {Concrete Semantics: With Isabelle/HOL},
 year = {2014},
 isbn = {3319105418, 9783319105413},
 publisher = {Springer Publishing Company, Incorporated},
} 

@book{Nipkow:2002:IPA:1791547,
 author = {Nipkow, Tobias and Wenzel, Markus and Paulson, Lawrence C.},
 title = {Isabelle/HOL: A Proof Assistant for Higher-order Logic},
 year = {2002},
 isbn = {3-540-43376-7},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
}
