Introducing robust reachability

Alur R, Henzinger TA, Kupferman O (2002) Alternating-time temporal logic. J ACM 49(5):672–713 Avgerinos T, Cha SK, Rebert A, Schwartz EJ, Woo M, Brumley D (2014) Automatic exploit generation. Communicat ACM 57(2):74–84 Aziz A, Sanwal K, Singhal V, Brayton R (1996) Verifying continuous time Markov chains. In: CAV. Springer Baldoni R, Coppa E, D’elia DC, Demetrescu C, Finocchi I (2018) A Survey of Symbolic Execution Techniques. ACM Comput Survey 51(3):1–39 Barret CW, Sebastiani R, Seshia SA, Tinelli C (2009) Satisfiability Modulo Theories. In: Handbook of Satisfiability. Ios press edn Barrett C, Conway CL, Deters M, Hadarean L, Jovanović D, King T, Reynolds A, Tinelli C (2011) CVC4. In: CAV. Springer Barthe G, D’Argenio P, Rezk T (2004) Secure information flow by self-composition. In CSF’04 Workshop Bradley AR, Manna Z, Sipma HB (2005) What’s Decidable About Arrays? In VMCAI. Springer Brillout A, Kroening D, Rümmer P, Wahl T (2011) Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic. In VMCAI. Springer Cadar C, Sen K (2013) Symbolic execution for software testing: three decades later. Communicat ACM 56(2):82–90 Cha SK, Avgerinos T, Rebert A, Brumley D (2012) Unleashing mayhem on binary Code. In S &P 2012 Chakraborty S, Meel K, Mistry R, Vardi M (2016) approximate probabilistic inference via Word-Level counting. AAAI 30(1) Cimatti A, Clarke EM, Giunchiglia F, Roveri M (1999) NuSMV: a new Symbolic Model Verifier. In CAV’99. Springer Clarke E, Kroening D, Lerda F (2004) A Tool for Checking ANSI-C Programs. In TACAS. Springer Clarke EM, Emerson EA (1982) Design and synthesis of synchronization skeletons using branching time temporal logic. In Logics of Programs. Springer Clarkson MR, Finkbeiner B, Koleini M, Micinski KK, Rabe MN, Sánchez C (2014) Temporal logics for hyperproperties. In principles of security and trust. Springer Clarkson MR, Schneider FB (2010) Hyperproperties. J Comput Secur 18(6):1157–1210 Cook B, Podelski A, Rybalchenko A (2006) Terminator: Beyond Safety. In: CAV. Springer Cowan C, Pu C, Maier D, Walpole J, Bakke P, Beattie S, Grier A, Wagle P, Zhang Q, Hinton H (1998) StackGuard: Automatic adaptive detection and prevention of buffer-overflow attacks. In USENIX Security Daniel LA, Bardin S, Rezk T (2020) Binsec/Rel: Efficient relational symbolic execution for constant-time at binary-level. In S &P 2020. IEEE David R, Bardin S, Ta TD, Mounier L, Feist J, Potet ML, Marion JY (2016) BINSEC/SE: A dynamic symbolic Execution toolkit for binary-level analysis. In SANER 2016. IEEE David R, Bardin S, Feist J, Mounier L, Potet ML, Ta TD, Marion JY (2016) Specification of concretization and symbolization policies in symbolic execution. In ISSTA 2016. ACM de Moura L, Bjørner N (2008) Z3: An Efficient SMT Solver. In TACAS. Springer Djoudi A, Bardin S (2015) BINSEC: Binary code analysis with low-level regions. In: TACAS. Springer Farinier B (2020) Decision Procedures for Vulnerability Analysis. Ph.D. thesis, Université Grenoble-Alpes Farinier B, Bardin S, Bonichon R, Potet ML (2018) Model generation for quantified formulas: a taint-based approach. In CAV. Springer Farinier B, David R, Bardin S, Lemerre M (2018) Arrays made simpler: an efficient, scalable and thorough Preprocessing. In LPAR-22 Ge Y, de Moura L (2009) Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories. In CAV. Springer Girol G, Farinier B, Bardin, S (2021) Not all bugs are created equal, but robust reachability can tell the difference. In CAV ’21. Springer Godefroid P (2011) Higher-order test generation. In PLDI ’11. ACM Godefroid P, Klarlund N, Sen K (2005) DART: directed automated random testing. In PLDI 2005. ACM Godefroid P, Levin MY, Molnar D (2012) SAGE: Whitebox fuzzing for security testing: SAGE has had a remarkable impact at Microsoft. Queue 10(1):20–27 Goguen JA, Meseguer J (1982) Security Policies and Security Models. In S &P 1982. IEEE Gomes CP, Sabharwal A, Selman B (2008) Model Counting. In Handbook of Satisfiability. Ios press edn Hansen T, Schachte P, Søndergaard H (2009) State Joining and Splitting for the Symbolic Execution of Binaries. In Runtime Verification. Springer Hansson H, Jonsson B (1994) A logic for reasoning about time and reliability. Formal Aspects o Comput 6(5):512–535 Hart S, Sharir M, Pnueli A (1983) Termination of Probabilistic Concurrent Program. ACM Transact Program Lang Syst 5(3):356–380 Heelan S (2009) Automatic generation of control flow hijacking exploits for software vulnerabilities. Master’s thesis, University of Oxford Heusser J, Malacaria P (2010) Quantifying information leaks in software. In ACSAC ’10. ACM Press Holler C, Herzig K, Zeller A (2012) Fuzzing with code fragments. In 21st USENIX security symposium. USENIX Association Kim S, McCamant S (2018) Bit-vector Model counting using statistical estimation. In TACAS. Springer Kurpiewski D, Knapik M, Jamroga W (2019) On Domination and Control in Strategic Ability. AAMAS .9 Laroussinie F, Meyer A, Petonnet E (2010) Counting CTL. In: Foundations of Software Science and Computational Structures. pp. 206–220. Lecture Notes in Computer Science Livshits B, Sridharan M, Smaragdakis Y, Lhoták O, Amaral JN, Chang BYE, Guyer SZ, Khedker UP, Møller A, Vardoulakis D (2015) In defense of soundiness: A manifesto. Communicat ACM 58(2):44–46 de Moura L, Bjørner N (2007) Efficient E-Matching for SMT Solvers. In Automated Deduction - CADE-21. Springer Niemetz A, Preiner M, Biere A (2015) Boolector 2.0: System description. J Satisf Boolean Modeling Comput 9(1) O’Hearn PW (2020) Incorrectness logic. POPL.4:1–32 Recoules F, Bardin S, Bonichon R, Mounier L, Potet ML (2019) Get Rid of Inline assembly through verification-oriented lifting. In ASE 2019. IEEE Reynolds A, Tinelli C, Goel A, Krstić S (2013) Finite model finding in SMT. In CAV. Springer Sen K, Marinov D, Agha G (2005) CUTE: a concolic unit testing engine for C. In ESEC/FSE-13. ACM Shoshitaishvili Y, Wang R, Salls C, Stephens N, Polino M, Dutcher A, Grosen J, Feng S, Hauser C, Kruegel C, Vigna G (2016) SOK: (State of) The art of war: Offensive techniques in binary analysis. In: SP 2016 Song F, Touili T (2014) Efficient CTL model-checking for pushdown systems. Theor Comput Sci 549:127–145 Urban C, Miné A (2017) Inference of ranking functions for proving temporal properties by abstract interpretation. Comput Lang Syst Struct 47:77–103 Urban C, Ueltschi S, Müller P (2018) Abstract interpretation of CTL properties. In SAS 2018. Springer Williams N, Marre B, Mouy P, Roger M (2005) Pathcrawler: Automatic generation of path tests by combining static and dynamic analysis. In EDCC-05. Springer