@book(BBook,
 author       = "J.-R. Abrial",
 year         = "1996",
 title        = "The {B}~Book - Assigning Programs to Meanings",
 publisher    = "Cambridge University Press",
 doi          = "10.1017/CBO9780511624162",
)
@article(nazareno02a,
 author       = "N.~Aguirre and T.~Maibaum",
 year         = "2002",
 title        = "A Temporal Logic Approach to the Specification of Reconfigurable Component-Based Systems",
 journal      = "Automated Software Engineering",
 doi          = "10.1109/ASE.2002.1115028",
)
@inproceedings(Aldric08,
 author       = "J.~Aldric",
 year         = "2008",
 title        = "Using Types to Enforce Architectural Structure",
 booktitle    = "WICSA'08",
 pages        = "23--34",
 doi          = "10.1109/WICSA.2008.48",
)
@inproceedings(BarringerGR07,
 author       = "H.~Barringer and D.~M. Gabbay and D.~E. Rydeheard",
 year         = "2007",
 title        = "From Runtime Verification to Evolvable Systems",
 booktitle    = "RV",
 series       = "LNCS",
 volume       = "4839",
 publisher    = "Springer",
 pages        = "97--110",
 doi          = "10.1007/978-3-540-77395-5\_9",
)
@article(DBLP:journals/adt/BarrosACHM09,
 author       = "T.~Barros and R.~Ameur-Boulifa and A.~Cansado and L.~Henrio and E.~Madelaine",
 year         = "2009",
 title        = "Behavioural models for distributed {Fractal} components",
 journal      = "Annales des T{\'e}l{\'e}communications",
 volume       = "64",
 number       = "1-2",
 pages        = "25--43",
 doi          = "10.1007/s12243-008-0069-7",
)
@inproceedings(DBLP:conf/wosp/BeckerKR07,
 author       = "S.~Becker and H.~Koziolek and R.~Reussner",
 year         = "2007",
 title        = "Model-Based performance prediction with the palladio component model",
 booktitle    = "Proceedings of the 6th International Workshop on Software and Performance, WOSP 2007",
 publisher    = "ACM",
 pages        = "54--65",
 doi          = "10.1145/1216993.1217006",
)
@inproceedings(DBLP:conf/euromicro/BradaV06,
 author       = "P.~Brada and L.~Valenta",
 year         = "2006",
 title        = "Practical Verification of Component Substitutability Using Subtype Relation",
 booktitle    = "32nd EUROMICRO Conference on Software Engineering and Advanced Applications, EUROMICRO-SEAA 2006",
 publisher    = "IEEE",
 pages        = "38--45",
 doi          = "10.1109/EUROMICRO.2006.50",
)
@article(Butler96,
 author       = "M.~J. Butler",
 year         = "1996",
 title        = "Stepwise Refinement of Communicating Systems",
 journal      = "Sci. Comput. Program.",
 volume       = "27",
 number       = "2",
 pages        = "139--173",
 doi          = "10.1016/0167-6423(96)81173-7",
)
@article(DBLP:journals/entcs/CernaVZ07,
 author       = "I.~Cern{\'a} and P.~Varekov{\'a} and B.~Zimmerova",
 year         = "2007",
 title        = "Component Substitutability via Equivalencies of Component-Interaction Automata",
 journal      = "Electr. Notes Theor. Comput. Sci.",
 volume       = "182",
 pages        = "39--55",
 doi          = "10.1016/j.entcs.2006.09.030",
)
@article(colin07a,
 author       = "S.~Colin and A.~Lanoix and J.~Souqui{\`e}res",
 year         = "2009",
 title        = "Trustworthy interface compliancy: data model adaptation",
 journal      = "Electronic Notes in Theoretical Computer Science",
 volume       = "203",
 number       = "7",
 pages        = "23--35",
 doi          = "10.1016/j.entcs.2009.03.024",
)
@inproceedings(aguilar01a,
 author       = "M.~Aguilar Cornejo and H.~Garavel and R.~Mateescu and N.~De Palma",
 year         = "2001",
 title        = "Specification and Verification of a Dynamic Reconfiguration Protocol for Agent-Based Applications",
 booktitle    = "DAIS",
 pages        = "229--244",
)
@inproceedings(dormoy10b,
 author       = "J.~Dormoy and O.~Kouchnarenko and A.~Lanoix",
 year         = "2010",
 title        = "Using Temporal Logic for Dynamic Reconfigurations of Components",
 booktitle    = "FACS 2010, 7th Int. Ws. on Formal Aspects of Component Software",
 series       = "LNCS",
 volume       = "6921",
 publisher    = "Springer",
 pages        = "200--217",
 doi          = "10.1007/978-3-642-27269-1\_12",
)
@inproceedings(dkl11:ip,
 author       = "J.~Dormoy and O.~Kouchnarenko and A.~Lanoix",
 year         = "2011",
 title        = "Runtime Verification of Temporal Patterns for Dynamic Reconfigurations of Components",
 booktitle    = "FACS 2011",
 series       = "LNCS",
 volume       = "7253",
 publisher    = "Springer",
 pages        = "115--132",
 doi          = "10.1007/978-3-642-35743-5\_8",
)
@inproceedings(dormoy12a,
 author       = "J.~Dormoy and O.~Kouchnarenko and A.~Lanoix",
 year         = "2012",
 title        = "{When Structural Refinement of Components Keeps Temporal Properties Over Reconfigurations}",
 booktitle    = "18th International Symposium on Formal Methods (FM 2012)",
 series       = "LNCS",
 volume       = "7436",
 publisher    = "Springer-Verlag",
 doi          = "10.1007/978-3-642-32759-9\_16",
)
@inproceedings(DBLP:conf/euromicro/FioukovEHC02,
 author       = "A.~V. Fioukov and E.M. Eskenazi and D.~K. Hammer and M.~R.~V. Chaudron",
 year         = "2002",
 title        = "Evaluation of Static Properties for Component-Based Architectures",
 booktitle    = "28th EUROMICRO Conference 2002",
 publisher    = "IEEE Computer Society",
 pages        = "33--39",
 url          = "http://computer.org/proceedings/euromicro/1787/17870033abs.htm",
)
@inproceedings(Glabbeek93,
 author       = "R.~J. van Glabbeek",
 year         = "1993",
 title        = "The Linear Time - Branching Time Spectrum II",
 booktitle    = "CONCUR '93, 4th International Conference on Concurrency Theory",
 series       = "LNCS",
 volume       = "715",
 publisher    = "Springer",
 pages        = "66--81",
 doi          = "10.1007/3-540-57208-2\_6",
)
@inproceedings(DBLP:conf/dagstuhl/GrassiMRS07,
 author       = "V.~Grassi and R.~Mirandola and E.~Randazzo and A.~Sabetta",
 year         = "2007",
 title        = "KLAPER: An Intermediate Language for Model-Driven Predictive Analysis of Performance and Reliability",
 booktitle    = "The Common Component Modeling Example: Comparing Software Component Models",
 series       = "LNCS",
 volume       = "5153",
 publisher    = "Springer",
 pages        = "327--356",
 doi          = "10.1007/978-3-540-85289-6\_13",
)
@book(Hamilton78,
 author       = "A.~G. Hamilton",
 year         = "1978",
 title        = "Logic for mathematicians",
 publisher    = "Cambridge University Press, Cambridge",
)
@article(hennessy85,
 author       = "M.~Hennessy and R.~Milner",
 year         = "1985",
 title        = "Algebraic Laws for Nondeterminism and Concurrency",
 journal      = "Journal of the ACM",
 volume       = "32",
 number       = "1",
 pages        = "137--161",
 doi          = "10.1145/2455.2460",
)
@inproceedings(KestenMP93,
 author       = "Y.~Kesten and Z.~Manna and A.~Pnueli",
 year         = "1994",
 title        = "Temporal Verification of Simulation and Refinement",
 booktitle    = "A Decade of Concurrency, Reflections and Perspectives, REX School/Symposium",
 series       = "LNCS",
 volume       = "803",
 publisher    = "Springer",
 pages        = "273--346",
 doi          = "10.1007/3-540-58043-3\_22",
)
@inproceedings(lanoix11a,
 author       = "A.~Lanoix and J.~Dormoy and O.~Kouchnarenko",
 year         = "2011",
 title        = "Combining Proof and Model-checking to Validate Reconfigurable Architectures",
 booktitle    = "FESCA 2011",
 series       = "ENTCS",
 doi          = "10.1016/j.entcs.2011.11.011",
)
@article(lanoix07b,
 author       = "A.~Lanoix and J.~Souqui{\`e}res",
 year         = "2008",
 title        = "A Trustworthy Assembly of Components using the {B} Refinement",
 journal      = "e-Informatica Software Engineering Journal (ISEJ)",
 volume       = "2",
 number       = "1",
 pages        = "9--28",
 url          = "http://www.e-informatyka.pl/attach/e-Informatica\_-\_Volume_2/Vol2Iss1Art1eInformatica.pdf",
)
@inproceedings(leger10a,
 author       = "M.~L{\'e}ger and Th. Ledoux and Th. Coupaye",
 year         = "2010",
 title        = "Reliable Dynamic Reconfigurations in a Reflective Component Model",
 booktitle    = "CBSE 2010",
 series       = "LNCS",
 volume       = "6092",
 pages        = "74--92",
 doi          = "10.1007/978-3-642-13238-4\_5",
)
@inproceedings(LeuschelB03,
 author       = "M.~Leuschel and M.~J. Butler",
 year         = "2003",
 title        = "{ProB}: A Model Checker for {B}",
 booktitle    = "Int. Symp. of Formal Methods Europe FME'03",
 series       = "LNCS",
 volume       = "2805",
 publisher    = "Springer",
 pages        = "855--874",
 doi          = "10.1007/978-3-540-45236-2\_46",
)
@inproceedings(LeuschelP07,
 author       = "M.~Leuschel and D.~Plagge",
 year         = "2007",
 title        = "Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more",
 booktitle    = "ISoLA'07",
 series       = "Revue des Nouvelles Technologies de l'Information",
 volume       = "RNTI-SM-1",
 pages        = "73--84",
)
@book(milner80,
 author       = "R.~Milner",
 year         = "1980",
 title        = "A Calculus of Communicating Systems",
 series       = "Lecture Notes in Computer Science",
 volume       = "92",
 publisher    = "Springer Verlag",
 doi          = "10.1007/3-540-10235-3",
)
@book(Milner:1989,
 author       = "R.~Milner",
 year         = "1989",
 title        = "Communication and Concurrency",
 publisher    = "Prentice-Hall, Inc.",
)
@inproceedings(park81,
 author       = "D.~Park",
 year         = "1981",
 title        = "Concurrency and Automata on Infinite Sequences",
 booktitle    = "Lecture Notes in Computer Science",
 volume       = "104",
 publisher    = "Springer Verlag",
 pages        = "167--183",
 doi          = "10.1007/BFb0017309",
)
@proceedings(DBLP:conf/cbse/2007,
 editor       = "H.~W. Schmidt and I.~Crnkovic and G.~T. Heineman and J.~A. Stafford",
 year         = "2007",
 title        = "Component-Based Software Engineering, 10th International Symposium, CBSE 2007, Medford, MA, USA, July 9-11, 2007, Proceedings",
 series       = "LNCS",
 volume       = "4608",
 publisher    = "Springer",
 doi          = "10.1007/978-3-540-73551-9",
)