Variational satisfiability solving: efficiently solving lots of related SAT problems

Acher M, Collet P, Lahire P, France RB (2011) slicing feature models. In: Proceeding Int’l conference on automated software engineering (ASE). IEEE, pp 424–427

Aloul FA, Ramani A, Markov IL, Sakallah KA (2002) Generic ilp versus specialized 0-1 ilp: an update. In: Proceedings of the 2002 IEEE/ACM international conference on computer-aided design, association for computing machinery, New York, ICCAD ’02, pp 450–457, https://doi.org/10.1145/774572.774638

Ananieva S, Kowal M, Thüm T, Schaefer I (2016) Implicit constraints in partial feature models. In: Int work on feature-oriented software development (FOSD), ACM, pp 18–27

Apel S, Scholz W, Lengauer C, Kästner C (2010) Language-independent reference checking in software product lines. In: Int work on feature-oriented software development (FOSD), ACM, pp 65–71

Ataei P, Termehchy A, Walkingshaw E (2017) Variational Databases. In: International Symp on database programming languages (DBPL), ACM, pp 11:1–11:4

Ataei P, Termehchy A, Walkingshaw E (2018) Managing structurally heterogeneous databases in software product lines. In: VLDB workshop: polystores and other systems for heterogeneous data (Poly)

Ataei P, Khan F, Walkingshaw E (2021) A variational database management system. In: ACM SIGPLAN int Conf on Generative Programming: concepts and Experiences (GPCE), to appear

Ataei P, Li Q, Walkingshaw E (2021) Should variation be encoded explicitly in databases?. In: Int working conf on variability modelling of software-intensive systems (VaMoS), pp 3:1–3:9

Austin TH, Flanagan C (2012) Multiple facets for dynamic information flow. In: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, pp 165–178

Austin TH, Yang J, Flanagan C, Solar-Lezama A (2013) Faceted execution of policy-agnostic programs. In: Proceedings of the eighth ACM SIGPLAN workshop on programming languages and analysis for security, association for computing machinery, New York, PLAS ’13, pP 15–26, https://doi.org/10.1145/2465106.2465121

Balyo T, Froleyks N, Heule M, Iser M, Järvisalo M, Suda M (eds) (2020) Proceedings of SAT Competition 2020: solver and benchmark descriptions. Department of computer science report series b department of computer science. University of Helsinki, Finland

Barrett C, Tinelli C (2018) Satisfiability modulo theories. In: Handbook of Model Checking. Springer, pp 305–343

Barrett C, Stump A, Tinelli C (2010) The SMT-LIB standard: version 2.0 Tech rep, Department of Computer Science. The University of Iowa, available at www.SMT-LIB.org

Barrett C, Conway CL, Deters M, Hadarean L, Jovanović D, King T, Reynolds A, Tinelli C (2011) cvc4. In: Gopalakrishnan G, Qadeer S (eds) Computer aided verification. springer, Heidelberg, pp 171–177

Barrett C, Fontaine P, Tinelli C (2016) The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org

Batory D (2005) Feature models, grammars, and propositional formulas. In: ACM SIGSOFT int systems and software product line conf (SPLC). Springer, pp 7–20

Benavides D, Ruiz-Cortés A, Trinidad P (2005) Automated reasoning on feature models. In: Proceeding int’l conference on advanced information systems engineering (CAiSE), pp 491–503

Benavides D, Segura S, Ruiz-Cortés A (2010) Automated analysis of feature models 20 years later: a literature review. Inform Syst 35(6):615–708

Biere A, Biere A, Heule M, Van Maaren H, Walsh T (2009) Handbook of satisfiability: vol 185 frontiers in artificial intelligence and applications. IOS Press

Bittner PM, Thüm T, Schaefer I (2019) Sat encodings of the at-most-k constraint. In: Ölveczky PC, Salaün G (eds) Software engineering and formal methods. Springer International Publishing, Cham, pp 127–144

Bodden E, Tolêdo T, Ribeiro M, Brabrand C, Borba P, Mezini M (2013 ) SPLLIFT: statically analyzing software product lines in minutes instead of years. In: Proceeding ACM SIGPLAN conf on programming language design and implementation (PLDI), ACM, pp 355–364

Brummayer R, Biere A (2009) Boolector: an efficient SMT solver for bit-vectors and arrays. In: Kowalewski S, Philippou A (eds) Tools and algorithms for the construction and analysis of systems, 15th international conference, TACAS 2009, held as part of the joint european conferences on theory and practice of software, ETAPS 2009, York, UK, 22-29 March 2009. Proceedings, Springer, lecture notes in computer science, vol 5505, pp 174–177, https://doi.org/10.1007/978-3-642-00768-2_16

Brummayer R, Biere A (2021) Boolector: a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions. https://boolector.github.io/ Accessed at 12 Sept 2021

Campora IIIJP, Chen S, Erwig M, Walkingshaw E (2018) Migrating gradual types. Proc of the ACM on Program Languages (PACMPL) Issue, ACM SIGPLAN Sympon Principles of Program Languages (POPL) 2:15:1–15:29

Campora IIIJP, Chen S, Walkingshaw E (2018) Casts and costs: harmonizing safety and performance in gradual typing. Proc of the ACM on Program Languages (PACMPL) issue, ACM SIGPLAN IntConfon Functional Program (ICFP) 2:98:1–98:30

Carmo Machado ID, McGregor JD, Cavalcanti YaC, De Almeida ES (2014) On strategies for testing software product lines: a systematic literature review. JInform Softw Technol (IST) 56(10):1183–1199

Chen S, Erwig M (2014) Counter-factual typing for debugging type errors. In: ACM SIGPLAN-SIGACT Symp on Principles of Program Languages, pp 583–594

Chen S, Erwig M, Walkingshaw E (2012) An error-tolerant type system for variational lambda calculus. In: ACM SIGPLAN Int Conf on Functional Program (ICFP), pp 29–40

Chen S, Erwig M, Smeltzer K (2014) Let’s hear both sides: on combining type-error reporting tools. In: IEEE int symp on visual languages and human-centric computing, pp 145–152

Chen S, Erwig M, Walkingshaw E (2014) Extending Type Inference to Variational Programs. ACM Trans Program Languages Syst 36(1):1:1–1:54

Chen S, Erwig M, Walkingshaw E (2016) A calculus for variational programming. In: European conference on object-oriented programming (ECOOP), LIPIcs, vol 56, pp 6:1–6:26

Chen S, Erwig M, Smeltzer K (2017) Exploiting diversity in type checkers for better error messages. J Vis Languages Comput 39:10–21

Claessen K, Hughes J (2000) Quickcheck: a lightweight tool for random testing of haskell programs. In: Proceedings of the fifth ACM SIGPLAN international conference on functional programming, association for computing machinery, New York, ICFP ’00, pp 268–279, https://doi.org/10.1145/351240.351266

Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst 8(2):244–263. https://doi.org/10.1145/5397.5399

Classen A, Cordy M, Schobbens PY, Heymans P, Legay A, Raskin JF (2013) Featured transition systems: foundations for verifying variability-intensive systems and their application to ltl model checking. IEEE Transon Softw Eng 39 (8):1069–1089

Coudert O, Madre JC (1995) New ideas for solving covering problems. In: Proceedings of the 32nd Annual ACM/IEEE design automation conference, association for computing machinery, New York, DAC ’95, pp 641–646. https://doi.org/10.1145/217474.217603

Czarnecki K, Pietroszek K (2006) Verifying feature-based model templates against well-formedness ocl constraints. In: ACM SIGPLAN conf on generative programming and component engineering. ACM, pp 211–220

Czarnecki K, Wȧsowski A (2007) Feature diagrams and logics: there and back again. In: ACM SIGSOFT Int systems and software product line conf (SPLC). IEEE, pp 23–34

Dutertre B (2014) Yices 2.2. In: Biere A, Bloem R (eds) Computer-aided verification (CAV’2014), Springer, lecture notes in computer science, vol 8559, pp 737–744

Eén N, Sörensson N (2003) Temporal induction by incremental sat solving. Electr Notes Theoretical Comput Sci 89(4):543–560

Eén N, Sörensson N (2004) An extensible sat-solver. In: Giunchiglia E, Tacchella A (eds) Theory and applications of satisfiability testing. Springer, Heidelberg, pp 502–518

Erkok L (2011) SBV: SMT Based Verification: Symbolic Haskell Theorem prover using SMT solving. Website available online at https://hackage.haskell.org/package/sbv-8.10; visited on 14th Feb 2020

Erwig M, Smeltzer K (2018) Variational Pictures. In: International conference on the theory and application of diagrams, LNAI 10871, pp 55–70

Erwig M, Walkingshaw E (2011) The choice calculus: a representation for software variation. ACM Trans Softw Eng Method (TOSEM) 21(1):6:1–6:27

Erwig M, Walkingshaw E, Chen S (2013) An abstract representation of variational graphs. In: Int work on feature-oriented software development (FOSD), ACM, pp 25–32

Fenske W, Meinicke J, Schulze S, Schulze S, Saake G (2017) Variant-preserving refactorings for migrating cloned products to a product line. In: ProcEEDING int’l conference on software analysis, evolution and reengineering (SANER). IEEE, pp 316–326

Galindo JA, Benavides D, Trinidad P, Gutiérrez-Fernández AM, Ruiz-Cortés A (2019) Automated analysis of feature models: quo vadis? Computing 101(5):387–433

Garson J (2018) Modal logic. In: Zalta EN (ed) The stanford encyclopedia of philosophy, fall 2018 edn., Metaphysics Research Lab, Stanford University

Gent IP, Walsh T (1994) The sat phase transition. In: In proceeding ECAI-94, pp 105–109

Hamming RW (1950) Error detecting and error correcting codes. Bell Syst Tech J 29(2):147–160

Harper R (2016) Practical foundations for programming languages. Cambridge University Press

Holm S (1979) A simple sequentially rejective multiple test procedure. Scandinavian J Stat 6(2):65–70. http://www.jstor.org/stable/4615733

Hooker JN (1993) Solving the incremental satisfiability problem. https://doi.org/10.1184/R1/6708044.v1, https://kilthub.cmu.edu/articles/journal_contribution/Solving_the_Incremental_Satisfiability_Problem/6708044/1

Huang SS, Zook D, Smaragdakis Y (2011) Statically Safe Program Generation with SafeGen. Sci Comput Program (SCP) 76(5):376–391

Hudak P, Peyton Jones S, Wadler P, Boutel B, Fairbairn J, Fasel J, Guzmán MM, Hammond K, Hughes J, Johnsson T, Kieburtz D, Nikhil R, Partain W, Peterson J (1992) Report on the programming language haskell: a non-strict. Purely Functional Lang Version 1.2. SIGPLAN Not 27(5):1–164. https://doi.org/10.1145/130697.130699

Huet G (1997) The zipper. J Functional Program 7(5):549–554. https://doi.org/10.1017/S0956796897002864

Kästner C, Giarrusso PG, Rendel T, Erdweg S, Ostermann K, Berger T (2011) Variability-Aware parsing in the presence of lexical macros and conditional compilation. In: Proceeding conference on object-oriented programming, systems, languages and applications (OOPSLA), ACM, pp 805–824

Kästner C, Ostermann K, Erdweg S (2012) A variability-Aware module system. In: Proceeding conference on object-oriented programming, systems, languages and applications(OOPSLA), ACM, pp 773–792

Kim J, Whittemore J, Marques-Silva J, Sakallah K (2000) On applying incremental satisfiability to delay fault testing. In: Proceedings of the conference on design, automation and test in europe, association for computing machinery, New York, Date ’00, pp 380–384, https://doi.org/10.1145/343647.343801

Kim J, Whittemore JP, Marques-Silva J, Sakallah KA (2000) On solving Stack-Based incremental satisfiability problems. In: Proceeding of IEEE international conference on computer design (ICCD). Austin, Texas, pp 379–382

Kleene SC (1968) Introduction to metamathematics. Ishi Press

Kocher P, Horn J, Fogh A, Genkin D, Gruss D, Haas W, Hamburg M, Lipp M, Mangard S, Prescher T, Schwarz M, Yarom Y (2019) Spectre attacks: exploiting speculative execution. In: 40th IEEE symposium on security and privacy (S&P’19)

Kowal M, Ananieva S, Thüm T (2016) Explaining anomalies in feature models. In: Proceeding int’l conference on generative programming: concepts & experiences (GPCE), ACM, pp 132–143

Krieter S, Schröter R, Thüm T, Fenske W, Saake G (2016) Comparing algorithms for efficient feature-model slicing. In: ACM SIGSOFT Int systems and software product line conf.(SPLC), ACM, pp 60–64

Krieter S, Thüm T, Schulze S, Schröter R, Saake G (2018) Propagating configuration decisions with modal implication graphs. In: Proc int’l conf on software engineering (ICSE), ACM, pp 898–909

Kästner C, Giarrusso PG, Ostermann K (2011) Partial preprocessing c code for variability analysis. In: In Proceeding 5th ACM workshop on variability modeling of software-intensive systems, pp 127–136

Labs R (2020) Redis. https://redis.io/, Accessed at 4th May 2020

Larabel M (2020) A global switch to kill linux’s CPU spectre/meltdown workarounds?. https://www.phoronix.com/scan.php?page=news_item&px=Global-Switch-Skip-Spectre-Melt, Accessed at 25th March 2020

Le Berre D, Parrain A (2010) The Sat4j Library. Release 2.2 7 (2-3):59–64

Levenshtein VI (1966) Binary codes capable of correcting deletions, insertions and reversals. Soviet Physics Doklady 10(8):707–710. doklady Akademii Nauk SSSR, V163 No4 845-848 1965

Liebig J, Kästner C, Apel S (2011) Analyzing the discipline of preprocessor annotations in 30 million lines of c code. In: Int. conf. on aspect-oriented software development, pp 191–202

Liebig J, von Rhein A, Kästner C, Apel S, Dörre J, Lengauer C (2013) Scalable analysis of variable software, ACM

Lin C L (1994) Hardness of approximating graph transformation problem. In: Du DZ, Zhang XS (eds) Algorithms and computation. Springer, Berlin, pp 74–82

Lipp M, Schwarz M, Gruss D, Prescher T, Haas W, Fogh A, Horn J, Mangard S, Kocher P, Genkin D, Yarom Y, Hamburg M (2018) Meltdown: Reading kernel memory from user space. In: 27th USENIX security symposium (USENIX Security 18)

Mauro J (2021) Anomaly detection in context-aware feature models. In: 15th international working conference on variability modelling of software-intensive systems. VaMoS’21, https://doi.org/10.1145/3442391.3442405. Association for Computing Machinery, New York

Mauro J, Nieke M, Seidl C, Yu IC (2017) Anomaly detection and explanation in context-aware software product lines. In: ACM SIGSOFT int. systems and software product line conf. (SPLC). ACM, pp 18–21

Medeiros F, Kästner C, Ribeiro M, Gheyi R, Apel S (2016) A comparison of 10 sampling algorithms for configurable systems. In: Proc. int’l conf. on software engineering (ICSE). ACM, pp 643–654

Meinicke J (2014) Varexj: a variability-aware interpreter for java applications. Master’s thesis, University of Magdeburg

Meinicke J (2019) Variational debugging: understanding differences among executions. PhD dissertation, University of Magdeburg

Mendonça M, Wa̧sowski A, Czarnecki K, Cowan D (2008) Efficient compilation techniques for large scale feature models. In: ACM SIGPLAN conf. on generative programming and component engineering. ACM, pp 13–22

Meng M, Meinicke J, Wong CP, Walkingshaw E, Kästner C (2017) A choice of variational stacks: exploring variational data structures. In: Int. work. on variability modelling of software-intensive systems (VaMoS). ACM, pp 28–35

Micinski K., Darais D., Gilray T (2020) Abstracting faceted execution. In: 2020 IEEE 33rd computer security foundations symposium (CSF). pp 184–198. https://doi.org/10.1109/CSF49147.2020.00021

Moskewicz MW, Madigan CF, Zhao Y, Zhang L, Malik S (2001) Chaff: Engineering an efficient sat solver. In: Proceedings of the 38th annual design automation conference, DAC ’01. ACM, New York, pp 530–535. https://doi.org/10.1145/378239.379017

de Moura L, Bjørner N (2008) Z3: an efficient smt solver. In: Ramakrishnan CR, Rehof J (eds) Tools and algorithms for the construction and analysis of systems. Springer, Heidelberg, pp 337–340

Nadel A, Ryvchin V, Strichman O (2014) Ultimately incremental sat. In: Sinz C, Egly U (eds) Theory and applications of satisfiability testing – SAT 2014. Springer International Publishing, Cham, pp 206–218

National Institute of Standards and Technology (2020) NIST e-handbook of statistical methods. https://www.itl.nist.gov/div898/handbook/index.htm, Accessed at 7th May 2020

Nguyen H V, Kästner C, Nguyen TN (2014) Exploring Variability-Aware execution for testing Plugin-Based web applications. In: Proc. int’l conf. on software engineering (ICSE), ACM, pp 907–918

Nieke M, Mauro J, Seidl C, Thüm T, Yu IC, Franzke F (2018) Anomaly analyses for feature-model evolution. In: ACM SIGPLAN Conf. on generative programming and component engineering, ACM, pp 188–201

O’Sullivan B (2009) Criterian: a Haskell Microbenchmarking library. Website available online at https://hackage.haskell.org/package/gauge-0.2.5; visited on 7th May 2020

R Core Team (2020) R: a language and environment for statistical computing. R foundation for statistical computing, Vienna, Austria, https://www.R-project.org/

Rescher N (1969) Many-Valued Logic. Mcgraw-Hill, New York

von Rhein A, Grebhahn A, Apel S, Siegmund N, Beyer D, Berger T (2015) Presence-Condition simplification in highly configurable systems. In: Proc. int’l conf. on software engineering (ICSE). IEEE, pp 178–188

Russell S, Norvig P (2009) Artificial Intelligence: A Modern Approach. 3rd edn. Prentice Hall Press, USA

Competition SAT (2021) SAT Competition 2021: incremental library track. https://satcompetition.github.io/2021/track_incremental.html. Accessed at 21 May 2022

Sayyad AS, Ingram J, Menzies T, Ammar H (2013) Scalable Product line configuration: a straw to break the camel’s back. In: Proc.int’l conf.on automated software engineering (ASE). IEEE, pp 465–474

Schmitz T, Algehed M, Flanagan C, Russo A (2018) Faceted secure multi execution. In: CCS ’18

Schröter R, Krieter S, Thüm T, Benduhn F, Saake G (2016) Feature-Model interfaces: the highway to compositional analyses of highly-configurable systems. In: Proc.int’l conf.on software engineering (ICSE), ACM, pp 667–678

Siegmund N, Rosenmüller M, Kuhlemann M, Kästner C, Apel S, Saake G (2012) SPL Conqueror: toward optimization of non-functional properties in software product lines. Softw Quality J (SQJ) 20(3-4):487–517

Smeltzer K, Erwig M (2017) Variational Lists: comparisons and design guidelines. In: ACM SIGPLAN Int. workshop on feature-oriented software development, pp 31–40

Tartler R, Lohmann D, Sincero J, Schröder-Preikschat W (2011) Feature consistency in compile-time-configurable system software: facing the linux 10,000 feature problem. In: Proc. europ. conf. on computer systems (EuroSys), ACM, pp 47–60

Thaker S, Batory D, Kitchin D, Cook W (2007) Safe composition of product lines. In: ACM SIGPLAN conf. on generative programming and component engineering, ACM, pp 95–104

Thüm T, Apel S, Kästner C, Schaefer I, Saake G (2014) A classification and survey of analysis strategies for software product lines. ACM Comput Surveys 47(1):6:1–6:45

Tinelli C (2003) The smt-lib format: an initial proposal. https://smtlib.cs.uiowa.edu/papers/pdpar-proposal.pdf, Accessed 28 September 2021

Varshosaz M, Al-Hajjaji M, Thüm T, Runge T, Mousavi MR, Schaefer I (2018) A classification of product sampling for software product lines. In: ACM SIGSOFT int. systems and software product line conf.(SPLC), ACM, pp 1–13

Visser W, Geldenhuys J, Dwyer MB (2012) Green: reducing, reusing and recycling constraints in program analysis. In: Proc. Int’l symposium on foundations of software engineering (FSE), ACM, pp 58:1–58:11

Walkingshaw E (2013) The choice calculus: a formal language of variation. PhD thesis, Oregon State University, http://hdl.handle.net/1957/40652

Walkingshaw E, Kästner C, Erwig M, Apel S, Bodden E (2014) Variational data structures: exploring trade-offs in computing with variability. In: ACM SIGPLAN Symp. on new ideas in programming and reflections on software (Onward!), pp 213–226

Whittemore J, Kim J, Sakallah K (2001) Satire: A new incremental satisfiability engine. In: Proceedings of the 38th annual design automation conference, association for computing machinery, New York, DAC ’01, pp 542–545, https://doi.org/10.1145/378239.379019

Wilcoxon F (1945) Individual comparisons by ranking methods. Biometrics Bulletin 1(6):80–83. http://www.jstor.org/stable/3001968

Wong CP (2021) Beyond configurable systems. Carnegie Mellon University, Applying variational execution to tackle large search spaces. PhD dissertation

Wong CP, Meinicke J, Lazarek L, Kästner C (2018) Faster variational execution with transparent bytecode transformation. Proc ACM Program Lang 2(OOPSLA), https://doi.org/10.1145/3276487

Young J (2021) Variational Satisfiability Solving. PhD thesis, Oregon State University, https://ir.library.oregonstate.edu/concern/graduate_thesis_or_dissertations/dv140182g?locale=en

Young JM, Walkingshaw E, Thüm T (2020) Variational satisfiability solving. In: Proceedings of the 24th acm conference on systems and softwar product line: volume a - volume a, association for computing machinery, New York, SPLC ’20, https://doi.org/10.1145/3382025.3414965

Zhang L, Madigan CF, Moskewicz MH, Malik S (2001) Efficient conflict driven learning in a boolean satisfiability solver. In: Proceedings of the 2001 IEEE/ACM international conference on computer-aided design, IEEE Press, Piscataway, NJ, USA, ICCAD ’01, pp 279–285, http://dl.acm.org/citation.cfm?id=603095.603153