@techreport{fgw11rapport-lri,
 author = "Abderrahmane Feliachi and Marie-Claude Gaudel and Burkhart Wolff",
 title = "Isabelle/Circus : a Process Specification and Verification Environment",
 year = 2011,
 number = 1547,
 address = "Universit{\'e} Paris-Sud XI",
 month = "November",
 note = "\url{http://www.lri.fr/~bibli/Rapports-internes/2011/RR1547.pdf}",
 x-equipes = "fortesse",
 x-type = "article",
 x-support = "rapport"
}

@inproceedings{DBLP:conf/vstte/FeliachiGW12,
  author    = {Abderrahmane Feliachi and
               Marie-Claude Gaudel and
               Burkhart Wolff},
  title     = {Isabelle/Circus: A Process Specification and Verification
               Environment},
  booktitle = {VSTTE},
  year      = {2012},
  pages     = {243-260},
  ee        = {https://doi.org/10.1007/978-3-642-27705-4_20},
  crossref  = {DBLP:conf/vstte/2012},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/vstte/2012,
  editor    = {Rajeev Joshi and
               Peter M{\"u}ller and
               Andreas Podelski},
  title     = {Verified Software: Theories, Tools, Experiments - 4th International
               Conference, VSTTE 2012, Philadelphia, PA, USA, January 28-29,
               2012. Proceedings},
  booktitle = {VSTTE},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {7152},
  year      = {2012},
  isbn      = {978-3-642-27704-7},
  ee        = {https://doi.org/10.1007/978-3-642-27705-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/vstte/FeliachiGW12,
  author    = {Abderrahmane Feliachi and
               Marie-Claude Gaudel and
               Burkhart Wolff},
  title     = {Isabelle/Circus: A Process Specification and Verification
               Environment},
  booktitle = {VSTTE},
  year      = {2012},
  pages     = {243-260},
  ee        = {https://doi.org/10.1007/978-3-642-27705-4_20},
  crossref  = {DBLP:conf/vstte/2012},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/vstte/2012,
  editor    = {Rajeev Joshi and
               Peter M{\"u}ller and
               Andreas Podelski},
  title     = {Verified Software: Theories, Tools, Experiments - 4th International
               Conference, VSTTE 2012, Philadelphia, PA, USA, January 28-29,
               2012. Proceedings},
  booktitle = {VSTTE},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {7152},
  year      = {2012},
  isbn      = {978-3-642-27704-7},
  ee        = {https://doi.org/10.1007/978-3-642-27705-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}



@inproceedings{Fischer:1998:CZP:647283.722938,
 author = {C. Fischer},
 title = {How to Combine {Z} with Process Algebra},
 booktitle = {11th Int. Conf. of Z Users on The Z Formal Specification Notation},
 year = {1998},
 isbn = {3-540-65070-9},
 pages = {5--23}, 
 acmid = {722938},
 publisher = {Springer-Verlag}
} 

@inproceedings{Taguchi:1997:SCS:523981.852142,
 author = {Taguchi, K. and Araki, K.},
 title = {The state-based {CCS} semantics for concurrent {Z} specification},
 booktitle = {ICFEM'97},
 year = {1997},
 isbn = {0-8186-8002-4},
 pages = {283--292},
 acmid = {852142},
 publisher = {IEEE},
 keywords = {Hennessy-Milner logic, Z notation, actions, calculus of communicating systems, concurrent systems specification, formal method, liveness, multiprocessing systems, process evolution, safety, state transitions, state-based CCS semantics, state-based semantics, value-passing CCS},
} 




@ARTICLE{Butler99csp2b:a,
    author = {M. Butler},
    title = {{CSP2B}: A Practical Approach To Combining {CSP} and {B}},
    journal = { Formal Aspects of Computing},
    year = {2000},
    volume = {12},
    pages = {182--196}
}

@book{HJ98,
  author =       "C. A. R. Hoare and He Jifeng",
  title =        "Unifying Theories of Programming",
  publisher =    "Prentice Hall International Series in Computer Science",
  year =         "1998"
}


@inproceedings{feliachi:uznifying-theories:2010,
  author = {A. Feliachi and M.-C. Gaudel and B. Wolff},
  title = {Unifying Theories in {I}sabelle/{HOL}},
  booktitle = {UTP 2010},
  publisher = {Springer Verlag},
  volume = {6445},
  series = {LNCS},
  year = {2010},
   pages = {188-206},
  pdf = {http://www.lri.fr/~feliachi/Papers/UTP10.pdf}
}



@article{CavalGau:Acta:2011,
  author    = {A. Cavalcanti and
               M.-C. Gaudel},
  title     = {Testing for refinement in {Circus}},
  journal   = {Acta Informatica},
  volume    = {48},
  number    = {2},
  year      = {2011},
  pages     = {97-147},
  pdf = {http://www.lri.fr/~mcg/PDF/CavalcantiGaudelCircus221110.pdf}
}



@Article{brucker.ea:theorem-prover:2012,
  author= {A. D. Brucker and B. Wolff},
  journal= {Formal Aspects of Computing},
  language= {USenglish},
  categories= {holtestgen},
  title= {On Theorem Prover-based Testing},
  year= {2012},
  classification= journal,
  areas= {formal methods, software},
  public= {yes},
  keywords= {test case generation, domain partitioning, test sequence,theorem proving, HOL-TestGen},
  pdf={http://www.brucker.ch/bibliography/download/2012/brucker.ea-theorem-prover-2012.pdf},
  note={To appear.},
  url={http://www.brucker.ch/bibliography/abstract/brucker.ea-theorem-prover-2012}  
}



@INPROCEEDINGS{SWC02,
AUTHOR = {A.~C.~A.~Sampaio and J.~C.~P.~Woodcock and A.~L.~C.~Cavalcanti},
TITLE = {Refinement in {C}ircus},
BOOKTITLE = {FME 2002},
YEAR = {2002},
VOLUME = {2391},
SERIES = {LNCS},
PAGES = {451---470},
PUBLISHER = {Springer},
}

@ARTICLE{CSW03,
AUTHOR = {A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio and J.~C.~P.~Woodcock},
TITLE = {{A Refinement Strategy for {\sf\textsl{Circus}}}},
JOURNAL = {Formal Aspects of Computing},
YEAR = {2003},
VOLUME = {15},
PAGES = {146 --- 181},
NUMBER = {2 - 3},
}


@book{Roscoe:1997:TPC:550448,
 author = {Roscoe, A. W. and Hoare, C. A. R. and Bird, Richard},
 title = {The  Theory and Practice of Concurrency},
 year = {1997},
 isbn = {0136744095},
 publisher = {Prentice Hall PTR},
 address = {Upper Saddle River, NJ, USA},
} 

@Book{            andrews:introduction:2002,
  author        = {P. B. Andrews},
  title         = {Introduction to Mathematical Logic and Type Theory: To
                  Truth through Proof},
  year          = 2002,
  isbn          = {1-402-00763-9},
  edition       = {2nd},
  publisher     = {Kluwer Academic},
  note       = {now published by Springer},
  acknowledgement={brucker, 2007-04-23},
  bibkey        = {andrews:introduction:2002}
}

@Article{         church:types:1940,
  author        = {A. Church},
  title         = {A formulation of the simple theory of types},
  journal       = {Journal of Symbolic Logic},
  year          = 1940,
  volume        = 5,
  number        = 2,
  month         = jun,
  pages         = {56--68},
  acknowledgement={brucker, 2007-04-23},
  bibkey        = {church:types:1940}
}

@Book{            nipkow.ea:isabelle:2002,
  author        = {T. Nipkow and L. C. Paulson and M. Wenzel},
  title         = {{Isabelle/HOL}---A Proof Assistant for Higher-Order
                  Logic},
  publisher     = {Springer-Verlag},
  series        = {LNCS},
  volume        = 2283,
  abstract      = {This book is a self-contained introduction to interactive
                  proof in higher-order logic (\acs{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/\acs{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. },
  myurl         = {http://www4.in.tum.de/~nipkow/LNCS2283/},
  year          = 2002,
  localurl      = {papers/2002/tutorial.pdf},
  acknowledgement={brucker, 2007-02-19},
  bibkey        = {nipkow.ea:isabelle:2002}
}

@article{CircusDS,
 author = {M. Oliveira and A.L.C. Cavalcanti and J.C.P. Woodcock},
 TITLE = {A Denotational Semantics for {C}ircus},
 journal = {Electron. Notes Theor. Comput. Sci.},
 volume = {187},
 year = {2007},
 issn = {1571-0661},
 pages = {107--123},
 doi = {https://doi.org/10.1016/j.entcs.2006.08.047},
 publisher = {Elsevier},
 }


@INPROCEEDINGS{CW06,
  AUTHOR = {A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
  TITLE = {{A Tutorial Introduction to {CSP} in Unifying Theories of Programming}},
  BOOKTITLE = {{Refinement Techniques in Software Engineering}},
  YEAR = {2006},
  VOLUME = {3167},
  SERIES = {LNCS},
  PAGES = {220 -- 268},
  PUBLISHER = {Springer-Verlag},
  GROUP = {utp},
  PDF = {./docs/cw06.pdf}
}

@INPROCEEDINGS{ZC09,
author = {F. Zeyda and A.L.C. Cavalcanti},
Title = {Encoding {C}ircus Programs in {P}roof{P}ower{Z}},
 booktitle = {
    {UTP} 2008},
series = {LNCS},
volume = {5713}, 
publisher = { Springer-Verlag},
year = {2009}
}


@article{Roggenbach:2006,
 author = {M. Roggenbach},
 title = {{CSP-CASL}: a new integration of process algebra and algebraic specification},
 journal = {Theor. Comput. Sci.},
 volume = {354},
 issue = {1},
 year = {2006},
 issn = {0304-3975},
 pages = {42--71},
 doi = {10.1016/j.tcs.2005.11.007},
 acmid = {1139752},
 publisher = {Elsevier},
 keywords = {CASL, CSP, algebraic specification, institution, process algebra}
} 


@INPROCEEDINGS{WC02,
AUTHOR = {J.~C.~P.~Woodcock and A.~L.~C.~Cavalcanti},
TITLE = {The Semantics of {Circus}},
BOOKTITLE = {ZB 2002},
YEAR = {2002},
VOLUME = {2272},
SERIES = {LNCS},
PAGES = {184---203},
PUBLISHER = {Springer-Verlag},
}