@inproceedings(AMS06,
 author       = "G.A. Agha and J. Meseguer and K. Sen",
 year         = "2005",
 title        = "{PMaude: Rewrite-based Specification Language for Probabilistic Object Systems}",
 booktitle    = "QAPL",
 series       = "ENTCS",
 volume       = "153",
 pages        = "213--239",
 doi          = "10.1016/j.entcs.2005.10.040",
)
@inproceedings(AM11,
 author       = "M. AlTurki and J. Meseguer",
 year         = "2011",
 title        = "{PVeStA: A Parallel Statistical Model Checking and Quantitative Analysis Tool}",
 editor       = "A. Corradini and B. Klin and C. C{\^{\i }}rstea",
 booktitle    = "CALCO",
 series       = "LNCS",
 volume       = "6859",
 publisher    = "Springer",
 pages        = "386--392",
 doi          = "10.1007/978-3-642-22944-2\_28",
)
@book(BK08,
 author       = "C. Baier and J.{-}P. Katoen",
 year         = "2008",
 title        = "Principles of Model Checking",
 publisher    = "The MIT Press",
 url          = "http://mitpress.mit.edu/books/principles-model-checking",
)
@inproceedings(Bat05,
 author       = "D.S. Batory",
 year         = "2005",
 title        = "{Feature Models, Grammars, and Propositional Formulas}",
 editor       = "J.H. Obbink and K. Pohl",
 booktitle    = "SPLC",
 series       = "LNCS",
 volume       = "3714",
 publisher    = "Springer",
 pages        = "7--20",
 doi          = "10.1007/11554844\_3",
)
@misc(BFGM15,
 author       = "M.H. {}ter Beek and A. Fantechi and S. Gnesi and F. Mazzanti",
 year         = "2015",
 title        = "{Modelling and Analysing the Variability in Product Families: Model Checking of Modal Transition Systems}",
 note         = "Submitted",
)
@inproceedings(BLP13,
 author       = "M.H. {}ter Beek and A. {Lluch Lafuente} and M. Petrocchi",
 year         = "2013",
 title        = "{Combining Declarative and Procedural Views in the Specification and Analysis of Product Families}",
 booktitle    = "FMSPLE workshop at SPLC",
 publisher    = "ACM",
 pages        = "10--17",
 doi          = "10.1145/2499777.2500722",
)
@inproceedings(BMS12,
 author       = "M.H. {}ter Beek and F. Mazzanti and A. Sulova",
 year         = "2012",
 title        = "{VMC: A Tool for Product Variability Analysis}",
 editor       = "D. Giannakopoulou and D. M{\'e}ry",
 booktitle    = "FM",
 series       = "LNCS",
 volume       = "7436",
 publisher    = "Springer",
 pages        = "450--454",
 doi          = "10.1007/978-3-642-32759-9\_36",
)
@inproceedings(BDV14b,
 author       = "M.H. {}{ter Beek} and E.P. de Vink",
 year         = "2014",
 title        = "{Software Product Line Analysis with mCRL2}",
 booktitle    = "SPLat workshop at SPLC",
 publisher    = "ACM",
 pages        = "78--85",
 doi          = "10.1145/2647908.2655970",
)
@inproceedings(BDV14a,
 author       = "M.H. {}ter Beek and E.P. de Vink",
 year         = "2014",
 title        = "{Using mCRL2 for the Analysis of Software Product Lines}",
 editor       = "S. Gnesi and N. Plat",
 booktitle    = "FormaliSE workshop at ICSE",
 publisher    = "IEEE",
 pages        = "31--37",
 doi          = "10.1145/2593489.2593493",
)
@inproceedings(MisscelAndPirlo,
 author       = "L. Belzner and R. {De Nicola} and A. Vandin and M. Wirsing",
 year         = "2014",
 title        = "{Reasoning (on) Service Component Ensembles in Rewriting Logic}",
 editor       = "S. Iida and J. Meseguer and K. Ogata",
 booktitle    = "Specification, Algebra, and Software",
 series       = "LNCS",
 volume       = "8373",
 publisher    = "Springer",
 pages        = "188--211",
 doi          = "10.1007/978-3-642-54624-2",
)
@article(BCLW13,
 author       = "P. Borba and M.B. Cohen and A. Legay and A. W\k {a}sowski",
 year         = "2013",
 title        = "{Analysis, Test and Verification in The Presence of Variability (Dagstuhl Seminar 13091)}",
 journal      = "Dagstuhl Reports",
 volume       = "3",
 number       = "2",
 pages        = "144--170",
 doi          = "10.4230/DagRep.3.2.144",
)
@inproceedings(Bor06,
 author       = "L. Bortolussi",
 year         = "2006",
 title        = "{Stochastic Concurrent Constraint Programming}",
 booktitle    = "QAPL",
 series       = "ENTCS",
 volume       = "164",
 pages        = "65--80",
 doi          = "10.1016/j.entcs.2006.07.012",
)
@inproceedings(BLLBGS14,
 author       = "J. B{\"{u}}rdek and S. Lity and M. Lochau and M. Berens and U. Goltz and A. Sch{\"{u}}rr",
 year         = "2014",
 title        = "{Staged Configuration of Dynamic Software Product Lines with Complex Binding Time Constraints}",
 editor       = "P. Collet and A. W\k {a}sowski and T. Weyer",
 booktitle    = "VaMoS",
 publisher    = "{ACM}",
 doi          = "10.1145/2556624.2556627",
)
@inproceedings(BM07,
 author       = "M.G. Buscemi and U. Montanari",
 year         = "2007",
 title        = "{CC-Pi: A Constraint-Based Language for Specifying Service Level Agreements}",
 editor       = "R. {De Nicola}",
 booktitle    = "ESOP",
 series       = "LNCS",
 volume       = "4421",
 publisher    = "Springer",
 pages        = "18--32",
 doi          = "10.1007/978-3-540-71316-6\_3",
)
@article(BM11,
 author       = "M.G. Buscemi and U. Montanari",
 year         = "2011",
 title        = "{QoS negotiation in service composition}",
 journal      = "J. Log. Algebr. Program.",
 volume       = "80",
 number       = "1",
 pages        = "13--24",
 doi          = "10.1016/j.jlap.2010.04.001",
)
@article(CCHLS12,
 author       = "A. Classen and M. Cordy and P. Heymans and A. Legay and P.{-}Y. Schobbens",
 year         = "2012",
 title        = "{Model checking software product lines with SNIP}",
 journal      = "STTT",
 volume       = "14",
 number       = "5",
 pages        = "589--612",
 doi          = "10.1007/s10009-012-0234-1",
)
@article(CCHLS14,
 author       = "A. Classen and M. Cordy and P. Heymans and A. Legay and P.{-}Y. Schobbens",
 year         = "2014",
 title        = "Formal semantics, modular specification, and symbolic verification of product-line behaviour",
 journal      = "Sci. Comput. Program.",
 volume       = "80",
 number       = "B",
 pages        = "416--439",
 doi          = "10.1145/2499777.2499781",
)
@article(CCSHLR13,
 author       = "A. Classen and M. Cordy and P.{-}Y. Schobbens and P. Heymans and A. Legay and J.{-}F. Raskin",
 year         = "2013",
 title        = "{Featured Transition Systems: Foundations for Verifying Variability-Intensive Systems and Their Application to LTL Model Checking}",
 journal      = "IEEE TSE",
 volume       = "39",
 number       = "8",
 pages        = "1069--1089",
 doi          = "10.1109/TSE.2012.86",
)
@proceedings(CDELMMT07,
 editor       = "M. {Clavel \emph {et al.}}",
 year         = "2007",
 title        = "{All About Maude --- A High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic}",
 series       = "LNCS",
 volume       = "4350",
 publisher    = "Springer",
 doi          = "10.1007/978-3-540-71999-1",
)
@inproceedings(CSHL13,
 author       = "M. Cordy and P.{-}Y. Schobbens and P. Heymans and A. Legay",
 year         = "2013",
 title        = "{Beyond Boolean Product-Line Model Checking: Dealing with Feature Attributes and Multi-features}",
 booktitle    = "ICSE",
 publisher    = "IEEE",
 pages        = "472--481",
 doi          = "10.1109/ICSE.2013.6606593",
)
@inproceedings(CHE04,
 author       = "K. Czarnecki and S. Helsen and U.W. Eisenecker",
 year         = "2004",
 title        = "{Staged Configuration Using Feature Models}",
 editor       = "R.L. Nord",
 booktitle    = "SPLC",
 series       = "LNCS",
 volume       = "3154",
 publisher    = "Springer",
 pages        = "266--283",
 doi          = "10.1007/978-3-540-28630-1\_17",
)
@inproceedings(DKB14,
 author       = "C. Dubslaff and S. Kl{\"{u}}ppelholz and C. Baier",
 year         = "2014",
 title        = "{Probabilistic Model Checking for Energy Analysis in Software Product Lines}",
 editor       = "W. Binder and E. Ernst and A. Peternier and R. Hirschfeld",
 booktitle    = "MODULARITY",
 publisher    = "ACM",
 pages        = "169--180",
 doi          = "10.1145/2577080.2577095",
)
@article(EW11,
 author       = "M. Erwig and E. Walkingshaw",
 year         = "2011",
 title        = "{The Choice Calculus: A Representation for Software Variation}",
 journal      = "ACM Trans. Softw. Eng. Methodol.",
 volume       = "21",
 number       = "1",
 eid          = "6",
 doi          = "10.1145/2063239.2063245",
)
@article(GS13,
 author       = "C. Ghezzi and A.M. Sharifloo",
 year         = "2013",
 title        = "Model-based verification of quantitative non-functional properties for software product lines",
 journal      = "Inform. Softw. Technol.",
 volume       = "55",
 number       = "3",
 pages        = "508--524",
 doi          = "10.1016/j.infsof.2012.07.017",
)
@inproceedings(DBLP:conf/ifm/GilmoreTV14,
 author       = "S. Gilmore and M. Tribastone and A. Vandin",
 year         = "2014",
 title        = "{An Analysis Pathway for the Quantitative Evaluation of Public Transport Systems}",
 editor       = "E. Albert and E. Sekerinski",
 booktitle    = "IFM",
 series       = "LNCS",
 volume       = "8739",
 publisher    = "Springer",
 pages        = "71--86",
 doi          = "10.1007/978-3-319-10181-1\_5",
)
@inproceedings(GP12,
 author       = "S. Gnesi and M. Petrocchi",
 year         = "2012",
 title        = "Towards an executable algebra for product lines",
 booktitle    = "FMSPLE workshop at SPLC",
 publisher    = "ACM",
 pages        = "66--73",
 doi          = "10.1145/2364412.2364424",
)
@techreport(KCHNP90,
 author       = "K.C. Kang and S.G. Cohen and J.A. Hess and W.E. Novak and A.S. Peterson",
 year         = "1990",
 title        = "{Feature-Oriented Domain Analysis (FODA) Feasibility Study}",
 type         = "Technical Report",
 number       = "CMU/SEI-90-TR-21",
 institution  = "Software Engineering Institute, Carnegie Mellon University",
 url          = "http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=11231",
)
@inproceedings(LL14,
 author       = "K.G. Larsen and A. Legay",
 year         = "2014",
 title        = "Statistical Model Checking: Past, Present, and Future",
 editor       = "T. Margaria and B. Steffen",
 booktitle    = "ISoLA",
 series       = "LNCS",
 volume       = "8802",
 publisher    = "Springer",
 pages        = "135--142",
 doi          = "10.1007/978-3-662-45231-8\_10",
)
@inproceedings(LDB10,
 author       = "A. Legay and B. Delahaye and S. Bensalem",
 year         = "2010",
 title        = "{Statistical Model Checking: An Overview}",
 editor       = "H. Barringer and Y. Falcone and B. Finkbeiner and K. Havelund and I. Lee and G.J. Pace and G. Rosu and O. Sokolsky and N. Tillmann",
 booktitle    = "RV",
 series       = "LNCS",
 volume       = "6418",
 publisher    = "Springer",
 pages        = "122--135",
 doi          = "10.1007/978-3-642-16612-9\_11",
)
@inproceedings(MB08,
 author       = "L. Mendon{\c {c}}a de Moura and N. Bj{\o }rner",
 year         = "2008",
 title        = "{Z3: An Efficient SMT Solver}",
 editor       = "C.R. Ramakrishnan and J. Rehof",
 booktitle    = "TACAS",
 series       = "LNCS",
 volume       = "4963",
 publisher    = "Springer",
 pages        = "337--340",
 doi          = "10.1007/978-3-540-78800-3\_24",
)
@inproceedings(MultivestaAlchemist,
 author       = "D. Pianini and S. Sebastio and A. Vandin",
 year         = "2014",
 title        = "{Distributed Statistical Analysis of Complex Systems Modeled Through a Chemical Metaphor}",
 booktitle    = "HPCS",
 publisher    = "{IEEE}",
 pages        = "416--423",
 doi          = "10.1109/HPCSim.2014.6903715",
)
@inproceedings(SR90,
 author       = "V.A. Saraswat and M.C. Rinard",
 year         = "1990",
 title        = "{Concurrent Constraint Programming}",
 editor       = "F.E. Allen",
 booktitle    = "POPL",
 publisher    = "ACM",
 pages        = "232--245",
 doi          = "10.1145/96709.96733",
)
@inproceedings(SB14,
 author       = "I. Schaefer and M.H. ter Beek",
 year         = "2014",
 title        = "{Fomal Methods and Analyses in Software Product Line Engineering}",
 editor       = "T. Margaria and B. Steffen",
 booktitle    = "ISoLA",
 series       = "LNCS",
 volume       = "8802",
 publisher    = "Springer",
 pages        = "253--256",
 doi          = "10.1007/978-3-662-45234-9\_18",
)
@inproceedings(SHT06,
 author       = "P.{-}Y. Schobbens and P. Heymans and J.{-}C. Trigaux",
 year         = "2006",
 title        = "{Feature Diagrams: A Survey and a Formal Semantics}",
 booktitle    = "RE",
 publisher    = "IEEE",
 pages        = "136--145",
 doi          = "10.1109/RE.2006.23",
)
@inproceedings(SEAMS2014,
 author       = "S. Sebastio and M. Amoretti and A. {Lluch Lafuente}",
 year         = "2014",
 title        = "{A Computational Field Framework for Collaborative Task Execution in Volunteer Clouds}",
 editor       = "G. Engels and N. Bencomo",
 booktitle    = "SEAMS workshop at ICSE",
 publisher    = "{ACM}",
 pages        = "105--114",
 doi          = "10.1145/2593929.2593943",
)
@inproceedings(SV13,
 author       = "S. Sebastio and A. Vandin",
 year         = "2013",
 title        = "{MultiVeStA: Statistical Model Checking for Discrete Event Simulators}",
 editor       = "A. Horvath and P. Buchholz and V. Cortellessa and L. Muscariello and M.S. Squillante",
 booktitle    = "ValueTools",
 publisher    = "ACM",
 pages        = "310--315",
 doi          = "10.4108/icst.valuetools.2013.254377",
)
@inproceedings(SVA05,
 author       = "K. Sen and M. Viswanathan and G.A. Agha",
 year         = "2005",
 title        = "{VESTA: A Statistical Model-checker and Analyzer for Probabilistic Systems}",
 booktitle    = "QEST",
 publisher    = "IEEE",
 pages        = "251--252",
 doi          = "10.1109/QEST.2005.42",
)
@article(TAKSS14,
 author       = "T. Th{\"u}m and S. Apel and C. K{\"a}stner and I. Schaefer and G. Saake",
 year         = "2014",
 title        = "{A Classification and Survey of Analysis Strategies for Software Product Lines}",
 journal      = "ACM Comput. Surv.",
 volume       = "47",
 number       = "1",
 eid          = "6",
 doi          = "10.1145/2580950",
)
@inproceedings(Tri14,
 author       = "M. Tribastone",
 year         = "2014",
 title        = "{Behavioral Relations in a Process Algebra for Variants}",
 editor       = "S. Gnesi and A. Fantechi and P. Heymans and J. Rubin and K. Czarnecki",
 booktitle    = "SPLC",
 publisher    = "ACM",
 pages        = "82--91",
 doi          = "10.1145/2648511.2648520",
)
@inproceedings(VK13,
 author       = "M. Varshosaz and R. Khosravi",
 year         = "2013",
 title        = "{Discrete Time Markov Chain Families: Modeling and Verification of Probabilistic Software Product Lines}",
 booktitle    = "FMSPLE workshop at SPLC",
 publisher    = "ACM",
 pages        = "34--41",
 doi          = "10.1145/2499777.2500725",
)