Dual analysis for proving safety and finding bugs

Godefroid, 1997, Model checking for programming languages using Verisoft, 174 Godefroid, 2005, DART: directed automated random testing, 213 Cousot, 1978, Automatic discovery of linear restraints among variables of a program, 84 Sankaranarayanan, 2006, Static analysis in disjunctive numerical domains, vol. 4134, 3 Blanchet, 2003, A static analyzer for large safety-critical software, 196 Rival, 2005, Understanding the origin of alarms in Astrée, vol. 3672, 303 Ball, 2001, Automatically validating temporal safety properties of interfaces, vol. 2057, 103 Henzinger, 2002, Lazy abstraction, 58 Clarke, 2000, Counterexample-guided abstraction refinement, 154 B.S. Gulavani, T.A. Henzinger, Y. Kannan, A.V. Nori, S.K. Rajamani, SYNERGY: a new algorithm for property checking, in: [51], pp. 117–127. Godefroid, 2010, Compositional may-must program analysis: unleashing the power of alternation, 43 Popeea, 2010, Dual analysis for proving safety and finding bugs, 2137 W. Kelly, V. Maslov, W. Pugh, et al., The Omega Library Version 1.1.0 Interface Guide, 1996. Pugh, 1992, A practical algorithm for exact array dependence analysis, Commun. ACM, 35, 102, 10.1145/135226.135233 Pugh, 1998, Constraint-based array dependence analysis, ACM Trans. Program. Lang. Syst., 20, 635, 10.1145/291889.291900 P. Cousot, R. Cousot, Modular static program analysis, in: [52], pp. 159–178. Gustavsson, 2001, Constraint abstractions, vol. 2053, 63 Hoare, 1969, An axiomatic basis for computer programming, Commun. ACM, 12, 576, 10.1145/363235.363259 Floyd, 1967, Assigning meanings to programs, 19, 10.1090/psapm/019/0235771 Dijkstra, 1975, Guarded commands, nondeterminacy and formal derivation of programs, Commun. ACM, 18, 453, 10.1145/360933.360975 Popeea, 2006, Inferring disjunctive postconditions, vol. 4435, 331 B. Hackett, A. Aiken, How is aliasing used in systems software?, in: [51], pp. 69–80. Gupta, 2008, Proving non-termination, 147 Nielson, 1999 G.C. Necula, S. McPeak, S.P. Rahul, W. Weimer, CIL: Intermediate language and tools for analysis and transformation of C programs, in: [52], pp. 213–228. Hall, 1992, The Glasgow Haskell Compiler: A retrospective, 62 Popeea, 2008, A practical and precise inference and specializer for array bound checks elimination, 177 National Institute of Standards and Technology, Java SciMark benchmark for scientific computing, 2004. http://math.nist.gov/scimark2/. Dongarra, 2003, The LINPACK benchmark: past, present and future, Concurrency and Computation: Practice and Experience, 15, 803, 10.1002/cpe.728 Beyer, 2007, The software model checker Blast, STTT, 9, 505, 10.1007/s10009-007-0044-z Ku, 2007, A buffer overflow benchmark for software model checkers, 389 Suzuki, 1977, Implementation of an array bound checker, 132 Cousot, 1976, Static determination of dynamic properties of programs, 106 Miné, 2006, The octagon abstract domain, Higher-Order and Symbolic Computation, 19, 31, 10.1007/s10990-006-8609-1 Venet, 2004, Precise and efficient static array bound checking for large embedded C programs, 231 Cadar, 2006, EXE: automatically generating inputs of death, 322 Xie, 2005, Scalable error detection using boolean satisfiability, 351 Godefroid, 2007, Compositional dynamic test generation, 47 Csallner, 2005, Check ’n’ crash: combining static checking and testing, 422 Flanagan, 2002, Extended static checking for Java, 234 Hovemeyer, 2004, Finding bugs is easy, SIGPLAN Notices, 39, 92, 10.1145/1052883.1052895 C. Popeea, Disjunctive invariants for modular static analysis, Ph.D. Thesis, Dept of Computer Science, National University of Singapore, 2008. Bourdoncle, 1993, Abstract debugging of higher-order imperative languages, 46 Rival, 2005, Abstract dependences for alarm diagnosis, vol. 3780, 347 I. Dillig, T. Dillig, A. Aiken, Sound, complete and scalable path-sensitive analysis, in: [53], pp. 270–280. S. Gulwani, S. Srivastava, R. Venkatesan, Program analysis as constraint solving, in: [53], pp. 281–292. Marriott, 1992, Bottom-up dataflow analysis of normal logic programs, J. Log. Program., 13, 181, 10.1016/0743-1066(92)90031-W Mernik, 2005, When and how to develop domain-specific languages, ACM Comput. Surv., 37, 316, 10.1145/1118890.1118892 Klint, 2009, Rascal: A domain specific language for source code analysis and manipulation, 168 Cousot, 1977, Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints, 238 2006 2002, vol. 2304 2008