@inproceedings(ABDFS13, author = {J.M. Atlee and S. Beidu and N.A. Day and F. Faghih and P. Shaker}, year = {2013}, title = {{Recommendations for Improving the Usability of Formal Methods for Product Lines}}, editor = {S. Gnesi and N. Plat}, booktitle = {FormaliSE}, publisher = {IEEE}, pages = {43--49}, doi = {10.1109/FormaliSE.2013.6612276}, ) @book(BHS07, author = {B. Beckert and R. H{\"a}hnle and P.H. Schmitt}, year = {2007}, title = {Verification of Object-Oriented Software: The KeY Approach}, publisher = {Springer}, doi = {10.1007/978-3-540-69061-0}, ) @inproceedings(BFGM15a, author = {{}ter Beek, M.H. and A. Fantechi and S. Gnesi and F. Mazzanti}, year = {2015}, title = {{Using FMC for Family-Based Analysis of Software Product Lines}}, editor = {D.C. Schmidt}, booktitle = {SPLC}, publisher = {ACM}, pages = {432--439}, doi = {10.1145/2791060.2791118}, ) @article(BFGM15b, author = {{}ter Beek, M.H. and A. Fantechi and S. Gnesi and F. Mazzanti}, year = {2016}, title = {Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints}, journal = {J. Log. Algebr. Meth. Program.}, volume = {85}, number = {2}, pages = {287--315}, doi = {10.1016/j.jlamp.2015.11.006}, ) @inproceedings(BLP13, author = {{}ter Beek, M.H. and {Lluch Lafuente}, A. and M. Petrocchi}, year = {2013}, title = {{Combining Declarative and Procedural Views in the Specification and Analysis of Product Families}}, editor = {D. Clarke}, booktitle = {FMSPLE}, series = {SPLC,}, volume = {2}, publisher = {ACM}, pages = {10--17}, doi = {10.1145/2499777.2500722}, ) @inproceedings(BMS12, author = {{}ter Beek, M.H. 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(BDV14c, author = {{}ter Beek, M.H. and E.P. de Vink}, year = {2014}, title = {{Towards Modular Verification of Software Product Lines with mCRL2}}, editor = {T. Margaria and B. Steffen}, booktitle = {ISoLA}, series = {LNCS}, volume = {8802}, publisher = {Springer}, pages = {368--385}, doi = {10.1007/978-3-662-45234-9\_26}, ) @inproceedings(BDV14a, author = {{}ter Beek, M.H. 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}, publisher = {IEEE}, pages = {31--37}, doi = {10.1145/2593489.2593493}, ) @inproceedings(BDVW16b, author = {{}ter Beek, M.H. and E.P. de Vink and T.A.C. Willemse}, year = {2016}, title = {Family-based model checking with {mCRL2}}, note = {Submitted}, ) @inproceedings(BBDV15, author = {T. Belder and M.H. ter Beek and E.P. de Vink}, year = {2015}, title = {{Coherent branching feature bisimulation}}, editor = {J.M. Atlee and S. Gnesi}, booktitle = {FMSPLE}, series = {EPTCS}, volume = {182}, pages = {14--30}, doi = {10.4204/EPTCS.182.2}, ) @article(BCLW13, author = {P. Borba and M.B. Cohen and A. Legay and A. Wasowski}, 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}, ) @incollection(BS01, author = {J.C. Bradfield and C. Stirling}, year = {2001}, title = {Modal Logics and $\mu$-Calculi: An Introduction}, editor = {J.A. Bergstra and A. Ponse and S.A. Smolka}, booktitle = {Handbook of Process Algebra}, chapter = {4}, publisher = {Elsevier}, pages = {293--330}, doi = {10.1016/B978-044482830-9/50022-9}, ) @book(CGP99, author = {E.M. Clarke and O. Grumberg and D.A. Peled}, year = {1999}, title = {Model Checking}, publisher = {The MIT Press}, ) @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 = {Int. J. Softw. Tools Technol. Transf.}, 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 Trans. Softw. Eng.}, volume = {39}, number = {8}, pages = {1069--1089}, doi = {10.1109/TSE.2012.86}, ) @inproceedings(CHSL11, author = {A. Classen and P. Heymans and P.{-}Y. Schobbens and A. Legay}, year = {2011}, title = {{Symbolic Model Checking of Software Product Lines}}, editor = {R.N. Taylor and H.C. Gall and N. Medvidovic}, booktitle = {ICSE}, publisher = {ACM}, pages = {321--330}, doi = {10.1145/1985793.1985838}, ) @inproceedings(CHSLR10, author = {A. Classen and P. Heymans and P.{-}Y. Schobbens and A. Legay and J.{-}F. Raskin}, year = {2010}, title = {{Model Checking \relax$\@@underline {\hbox{Lots}}\mathsurround\z@ $\relax of Systems: Efficient Verification of Temporal Properties in Software Product Lines}}, editor = {J. Kramer and J. Bishop and P.T. Devanbu and S. Uchitel}, booktitle = {ICSE}, publisher = {ACM}, pages = {335--344}, doi = {10.1145/1806799.1806850}, ) @inproceedings(CCHSL13, author = {M. Cordy and A. Classen and P. Heymans and P.{-}Y. Schobbens and A. Legay}, year = {2013}, title = {{ProVeLines: a product line of verifiers for software product lines}}, booktitle = {SPLC}, volume = {2}, publisher = {ACM}, pages = {141--146}, doi = {10.1145/2499777.2499781}, ) @inproceedings(CGKSVWW13, author = {S. Cranen and J.F. Groote and J.J.A. Keiren and F.P.M. Stappers and E.P. de Vink and W. Wesselink and T.A.C. Willemse}, year = {2013}, title = {{An Overview of the mCRL2 Toolset and Its Recent Advances}}, editor = {N. Piterman and S.A. Smolka}, booktitle = {TACAS}, series = {LNCS}, volume = {7795}, publisher = {Springer}, pages = {199--213}, doi = {10.1007/978-3-642-36742-7\_15}, ) @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}, ) @inproceedings(FUB06, author = {D. Fischbein and S. Uchitel and V.A. Braberman}, year = {2006}, title = {A foundation for behavioural conformance in software product line architectures}, editor = {R.M. Hierons and H. Muccini}, booktitle = {ROSATEA}, publisher = {ACM}, pages = {39--48}, doi = {10.1145/1147249.1147254}, ) @inproceedings(GM98, author = {J.F. Groote and R. Mateescu}, year = {1999}, title = {{Verification of Temporal Properties of Processes in a Setting with Data}}, editor = {A.M. Haeberer}, booktitle = {AMAST}, series = {LNCS}, volume = {1548}, publisher = {Springer}, pages = {74--90}, doi = {10.1007/3--540--49253--4\_8}, ) @book(GM14, author = {J.F. Groote and M.R. Mousavi}, year = {2014}, title = {Modeling and Analysis of Communicating Systems}, publisher = {The MIT Press}, ) @article(GW05, author = {J.F. Groote and T.A.C. Willemse}, year = {2005}, title = {Model-checking processes with data}, journal = {Sci. Comput. Program.}, volume = {56}, number = {3}, pages = {251--273}, doi = {10.1016/j.scico.2004.08.002}, ) @article(Koz83, author = {D. Kozen}, year = {1983}, title = {Results on the propositional $\mu$-calculus}, journal = {Theoret. Comput. Sci.}, volume = {27}, number = {3}, pages = {333--354}, doi = {10.1016/0304--3975(82)90125--6}, ) @inproceedings(LNW07, author = {K.G. Larsen and U. Nyman and A. Wasowski}, year = {2007}, title = {{Modal I/O Automata for Interface and Product Line Theories}}, editor = {{De Nicola}, R.}, booktitle = {ESOP}, series = {LNCS}, volume = {4421}, publisher = {Springer}, pages = {64--79}, doi = {10.1007/978-3-540-71316-6\_6}, ) @inproceedings(LPT09, author = {K. Lauenroth and K. Pohl and S. T{\"o}hning}, year = {2009}, title = {{Model Checking of Domain Artifacts in Product Line Engineering}}, booktitle = {ASE}, publisher = {IEEE}, pages = {269--280}, doi = {10.1109/ASE.2009.16}, ) @inproceedings(LT12, author = {M. Leucker and D. Thoma}, year = {2012}, title = {{A Formal Approach to Software Product Families}}, editor = {T. Margaria and B. Steffen}, booktitle = {ISoLA}, series = {LNCS}, volume = {7609}, publisher = {Springer}, pages = {131--145}, doi = {10.1007/978-3-642-34026-0\_11}, ) @inproceedings(LMBR14, author = {M. Lochau and S. Mennicke and H. Baller and L. Ribbeck}, year = {2014}, title = {{DeltaCCS: A Core Calculus for Behavioral Change}}, editor = {T. Margaria and B. Steffen}, booktitle = {ISoLA}, series = {LNCS}, volume = {8802}, publisher = {Springer}, pages = {320--335}, doi = {10.1007/978-3-662-45234-9\_23}, ) @article(LMBR16, author = {M. Lochau and S. Mennicke and H. Baller and L. Ribbeck}, year = {2016}, title = {{Incremental model checking of delta-oriented software product lines}}, journal = {J. Log. Algebr. Meth. Program.}, volume = {85}, number = {1}, pages = {245--267}, doi = {10.1016/j.jlamp.2015.09.004}, ) @article(SH11, author = {I. Schaefer and R. H{\"a}hnle}, year = {2011}, title = {Formal Methods in Software Product Line Engineering}, journal = {IEEE Comp.}, volume = {44}, number = {2}, pages = {82--85}, doi = {10.1109/MC.2011.47}, ) @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}, pages = {6:1--6:45}, doi = {10.1145/2580950}, ) @inproceedings(TSHA12, author = {T. Th{\"{u}}m and I. Schaefer and M. Hentschel and S. Apel}, year = {2012}, title = {Family-Based Deductive Verification of Software Product Lines}, editor = {K. Ostermann and W. Binder}, booktitle = {GPCE}, publisher = {ACM}, pages = {11--20}, doi = {10.1145/2371401.2371404}, ) @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}, )