Papers

KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs. 2008

C. Cadar, D. Dunbar, D. Engler

PDF
ACM

Z3: An Efficient SMT Solver. 2008

L. De Moura, N. Bjørner

PDF
ACM

An Extensible SAT-solver. 2004

N. Eén, N. Sörensson

PDF

S2E: A Platform for In-vivo Multi-path Analysis of Software Systems. 2011

V. Chipounov, V. Kuznetsov, G. Candea

PDF
ACM

DART: Directed Automated Random Testing. 2005

P. Godefroid, N. Klarlund, K. Sen

PDF
ACM

LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. 2004

C. Lattner, V. Adve

PDF
ACM

All You Ever Wanted to Know About Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask). 2010

E. Schwartz, T. Avgerinos, D. Brumley

PDF
ACM

Unleashing Mayhem on Binary Code. 2012

S. Cha, T. Avgerinos, A. Rebert, D. Brumley

PDF
ACM

On computable numbers, with an application to the Entscheidungsproblem. 1937

A. Turing

PDF

Pin: building customized program analysis tools with dynamic instrumentation. 2005

C. Luk, R. Cohn, R. Muth, H. Patil, A. Klauser, G. Lowney, S. Wallace, V. Reddi, K. Hazelwood

PDF
ACM

(State of) The Art of War: Offensive Techniques in Binary Analysis. 2016

Y. Shoshitaishvili, R. Wang, C. Salls, N. Stephens, M. Polino, A. Dutcher, J. Grosen, S. Feng, C. Hauser, C. Kruegel, G. Vigna

JPF-SE: A Symbolic Execution Extension to Java PathFinder. 2007

S. Anand, C. Păsăreanu, W. Visser

PDF
ACM

Test Input Generation with Java PathFinder. 2004

W. Visser, C. Păsăreanu, S. Khurshid

PDF
ACM

Green: Reducing, Reusing and Recycling Constraints in Program Analysis. 2012

W. Visser, J. Geldenhuys, M. Dwyer

PDF
ACM

Driller: Augmenting Fuzzing Through Selective Symbolic Execution. 2016

N. Stephens, J. Grosen, C. Salls, A. Dutcher, R. Wang, J. Corbetta, Y. Shoshitaishvili, C. Kruegel, G. Vigna

PDF

CUTE: A Concolic Unit Testing Engine for C. 2005

K. Sen, D. Marinov, G. Agha

PDF
ACM

Symbolic PathFinder: Symbolic Execution of Java Bytecode. 2010

C. Păsăreanu, N. Rungta

PDF
ACM

The RoadRunner Dynamic Analysis Framework for Concurrent Programs. 2010

C. Flanagan, S. Freund

PDF
ACM

DroidScope: Seamlessly Reconstructing the OS and Dalvik Semantic Views for Dynamic Android Malware Analysis. 2012

Lok Kwong Yan, Heng Yin

PDF

PEBIL: Efficient static binary instrumentation for Linux. 2010

M. A. Laurenzano, M. M. Tikir, L. Carrington, A. Snavely

Enhancing Symbolic Execution with Veritesting. 2014

T. Avgerinos, A. Rebert, S. Cha, D. Brumley

PDF
ACM

A System to Generate Test Data and Symbolically Execute Programs. 1976

L. A. Clarke

PDF

Computation beyond Turing machines. 2003

P. Wegner, D. Goldin

PDF

TaintDroid: An Information-flow Tracking System for Realtime Privacy Monitoring on Smartphones. 2010

W. Enck, P. Gilbert, B. Chun, L. Cox, J. Jung, P. McDaniel, A. Sheth

PDF
ACM

Testing for Buffer Overflows with Length Abstraction. 2008

R. Xu, P. Godefroid, R. Majumdar

PDF
ACM

CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-checking Tools. 2006

K. Sen, G. Agha

PDF
ACM

Under-constrained Symbolic Execution: Correctness Checking for Real Code. 2015

D. Ramos, D. Engler

PDF
ACM

Firmalice - Automatic Detection of Authentication Bypass Vulnerabilities in Binary Firmware. 2015

Y. Shoshitaishvili, R. Wang, C. Hauser, C. Kruegel, G. Vigna

PDF

Combined Static and Dynamic Automated Test Generation. 2011

PDF

Automatic Exploit Generation. 2014

T. Avgerinos, S. Cha, A. Rebert, E. Schwartz, M. Woo, D. Brumley

PDF
ACM

DyTa: Dynamic Symbolic Execution Guided with Static Verification Results. 2011

PDF

Mixed Abstractions for Floating-Point Arithmetic. 2009

PDF

A Systematic Study of Automated Program Repair: Fixing 55 out of 105 Bugs for $8 Each. 2012

C. Le Goues, M. Dewey-Vogt, S. Forrest, W. Weimer

PDF
ACM

Replayer: Automatic Protocol Replay by Binary Analysis. 2006

J. Newsome, D. Brumley, J. Franklin, D. Song

PDF
ACM

High coverage detection of input-related security faults. 2003

E. Larson, T. Austin

PDF

Loop-extended Symbolic Execution on Binary Programs. 2009

P. Saxena, P. Poosankam, S. McCamant, D. Song

PDF
ACM

A Symbolic Java Virtual Machine for Test Case Generation. 2004

R. Müller, C. Lembeck, H. Kuchen

PDF

EXE: Automatically Generating Inputs of Death. 2006

C. Cadar, V. Ganesh, P. Pawlowski, D. Dill, D. Engler

PDF
ACM

Symbolic Execution and Program Testing. 1976

J. King

PDF
ACM

DTA++: Dynamic Taint Analysis with Targeted Control-Flow Propagation. 2011

Min Gyung Kang, S. McCamant, P. Poosankam, D. Song

PDF

CalFuzzer: An extensible active testing framework for concurrent programs. 2009

P. Joshi, M. Naik, C. Park, K. Sen

KLOVER: A Symbolic Execution and Automatic Test Generation Tool for C++ Programs. 2011

G. Li, I. Ghosh, S. Rajan

PDF
ACM

A Comparative Study of Incremental Constraint Solving Approaches in Symbolic Execution. 2014

T. Liu, M. jo, M. d'Amorim, M. Taghdiri

PDF

JDart: A Dynamic Symbolic Analysis Framework. 2016

K. Luckow, M. Dimjašević, D. Giannakopoulou, F. Howar, M. Isberner, T. Kahsai, Z. Rakamarić, V. Raman

PDF

Event Listener Analysis and Symbolic Execution for Testing GUI Applications. 2009

S. Ganov, C. Killmar, S. Khurshid, D. Perry

PDF
ACM

Simplify: A Theorem Prover for Program Checking. 2005

D. Detlefs, G. Nelson, J. Saxe

PDF
ACM

Javana: A System for Building Customized Java Program Analysis Tools. 2006

J. Maebe, D. Buytaert, L. Eeckhout, K. De Bosschere

PDF
ACM

Sherlock: Scalable Deadlock Detection for Concurrent Programs. 2014

M. Eslamimehr, J. Palsberg

PDF
ACM

Z3-str: A Z3-based String Solver for Web Application Analysis. 2013

Y. Zheng, X. Zhang, V. Ganesh

PDF
ACM

Catchconv: Symbolic execution and run-time type inference for integer conversion errors. 2007

D. Molnar, D. Wagner

PDF

Flayer: Exposing Application Internals. 2007

W. Drewry, T. Ormandy

PDF
ACM

A Survey of Symbolic Execution Techniques. 2016

PDF
Arxiv

Equivalence Problems in a Model of Computation. 1967

M. Paterson

PDF

Efficient State Merging in Symbolic Execution. 2012

V. Kuznetsov, J. Kinder, S. Bucur, G. Candea

ACM

PySMT: a Solver-Agnostic Library for Fast Prototyping of SMT-Based Algorithms. 2015

M. Gario, A. Micheli

PDF

On Tracking Information Flows Through JNI in Android Applications. 2014

C. Qian, X. Luo, Y. Shao, A. Chan

PDF
ACM

Theory and Techniques for Automatic Generation of Vulnerability-Based Signatures. 2008

D. Brumley, J. Newsome, D. Song, H. Wang, S. Jha

PDF

Rex: Symbolic Regular Expression Explorer. 2010

M. Veanes, P. Halleux, N. Tillmann

PDF
ACM

Автоматизированный метод построения эксплойтов для уязвимости переполнения буфера на стеке. 2014

В. Падарян, В. Каушан, А. Федотов

PDF

Soot - a Java Bytecode Optimization Framework. 1999

R. Vallée-Rai, P. Co, E. Gagnon, L. Hendren, P. Lam, V. Sundaresan

PDF
ACM

Directed Symbolic Execution. 2011

K. Ma, K. Phang, J. Foster, M. Hicks

PDF
ACM

Symbolic Execution of Multithreaded Programs from Arbitrary Program Contexts. 2014

T. Bergan, D. Grossman, L. Ceze

PDF
ACM

FloPSy - Search-Based Floating Point Constraint Solving for Symbolic Execution. 2010

K. Lakhotia, N. Tillmann, M. Harman, J. de Halleux

PDF

The BORG: Nanoprobing Binaries for Buffer Overreads. 2015

M. Neugschwandtner, P. Milani Comparetti, I. Haller, H. Bos

PDF
ACM

An Empirical Study of Path Feasibility Queries. 2013

A. Sharma

PDF
Arxiv

Building Java Program Analysis Tools Using Javana. 2006

D. Buytaert, J. Maebe, L. Eeckhout, K. De Bosschere

PDF
ACM

Guiding Dynamic Symbolic Execution toward Unverified Program Executions. 2016

M. Christakis, P. Müller, V. Wüstholz

PDF
ACM

Higher-order Symbolic Execution via Contracts. 2012

S. Tobin-Hochstadt, D. Van Horn

PDF
ACM

Heap Cloning: Enabling Dynamic Symbolic Execution of Java Program. 2011

PDF

ExpliSAT: Guiding SAT-based Software Verification with Explicit States. 2006

S. Barner, C. Eisner, Z. Glazberg, D. Kroening, I. Rabinovitz

PDF
ACM

'ecution concolique et d’analyses en runtime. 2015

J. Salwan, F. Saudel

PDF

Automatic Low Overhead Program Instrumentation with the LOPI Framework. 2005

S. Kagstrom, H. Grahn, L. Lundberg

PDF
ACM

Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. 1977

P. Cousot, R. Cousot

PDF
ACM

DSD-Crasher: A Hybrid Analysis Tool for Bug Finding. 2006

C. Csallner, Y. Smaragdakis

PDF
ACM

Send Hardest Problems My Way: Probabilistic Path Prioritization for Hybrid Fuzzing. 2009

L. Zhao, Y. Duan, H. Yin, J. Xuan

PDF

Related terms search based on WordNet / Wiktionary and its application in Ontology Matching. 2009

A. A. Krizhanovsky, F. Lin

Fuzzing: Art, Science, and Engineering. 2018

Valentin J. M. s, HyungSeok Han, Choongwoo Han, Sang Kil Cha, Manuel Egele, Edward J. Schwartz, Maverick Woo

Межпроцедурный контекстно-чувствительный статический анализ для поиска ошибок в исходном коде программ на языках Си и Си++. 2016

А. Бородин

PDF

Внутрипроцедурный анализ для поиска ошибок на основе символьного выполнения. 2019

А. Бородин

JDriver: Automatic Driver Class Generation for AFL-Based Java Fuzzing Tools. 2018

Z. Huang, Y. Wang

Smart Greybox Fuzzing. 2018

V. Pham, M. Böhme, A. Santosa, A. Căciulescu, A. Roychoudhury

PDF
Arxiv

ARTist: The Android runtime instrumentation and security toolkit. 2017

M. Backes, S. Bugiel, O. Schranz, P. von Styp-Rekowsky, S. Weisgerber

PDF
Arxiv

Assisting in Auditing of Buffer Overflow Vulnerabilities via Machine Learning. 2017

Q. Meng, C. Feng, B. Zhang, C. Tang

Survey of Automated Vulnerability Detection and Exploit Generation Techniques in Cyber Reasoning Systems. 2017

T. Brooks

PDF
Arxiv

The Mayhem Cyber Reasoning System. 2018

T. Avgerinos, D. Brumley, J. Davis, R. Goulden, T. Nighswander, A. Rebert, N. Williamson

The Art of Computer Programming, Volume 1 (3rd Ed.): Fundamental Algorithms. 1997

D. Knuth

PLDI 2002: Extended Static Checking for Java. 2013

C. Flanagan, K. Leino, M. Lillibridge, G. Nelson, J. Saxe, R. Stata

ACM

Measuring Channel Capacity to Distinguish Undue Influence. 2009

J. Newsome, S. McCamant, D. Song

PDF
ACM

Using Dynamic Symbolic Execution to Improve Deductive Verification. 2008

D. Vanoverberghe, N. Bjørner, J. de Halleux, W. Schulte, N. Tillmann

Discovering Application-Level Insider Attacks Using Symbolic Execution. 2009

Proving Memory Safety of the ANI Windows Image Parser Using Compositional Exhaustive Testing. 2015

Execution Synthesis: A Technique for Automated Software Debugging. 2010

Symbolic Query Exploration. 2009

Temporal search: detecting hidden malware timebombs with virtual machines. 2006

A Framework for Automated Architecture-independent Gadget Search. 2010

T. Dullien, T. Kornau, R. Weinmann

ACM

Better bug reporting with better privacy. 2008

Dynamically validating static memory leak warnings. 2012

Symbolic Execution for Software Testing in Practice: Preliminary Assessment. 2011

C. Cadar, P. Godefroid, S. Khurshid, C. Păsăreanu, K. Sen, N. Tillmann, W. Visser

ACM

lp_solve: Mixed Integer Linear Programming solver. 2003

Autodafé: an Act of Software Torture. 2005

M. Vuagnoux

PDF

Probabilistic symbolic execution. 2012

Detecting Security Vulnerabilities in Web Applications Using Dynamic Analysis with Penetration Testing. 2008

PDF

Toward Automated Detection of Logic Vulnerabilities in Web Applications. 2010

The MATHSAT 4 SMT solver: Tool paper. 2008

R. Bruttomesso, A. Cimatti, A. Franzén, A. Griggio, R. Sebastiani

PDF

A Search-Based Framework for Failure Reproduction. 2012

Efficient Testing of Concurrent Programs with Abstraction-Guided Symbolic Execution. 2009

Symbolic Execution with Interval Solving and Meta-heuristic Search. 2012

Statically-Directed Dynamic Automated Test Generation. 2011

Memoized symbolic execution. 2012

Mcsema: Static translation of x86 instructions to llvm. 2014

A. Dinaburg, A. Ruef

Sound, Complete and Scalable Path-sensitive Analysis. 2008

I. Dillig, T. Dillig, A. Aiken

PDF
ACM

Program Analysis via Satisfiability Modulo Path Programs. 2010

HadoopToSQL: a mapReduce query optimizer. 2010

Context-Sensitive Relevancy Analysis for Efficient Symbolic Execution. 2008

Generalized Symbolic Execution for Model Checking and Testing. 2003

No Java without caffeine: A tool for dynamic analysis of Java programs. 2002

Y. G. Gueheneuc, R. Douence, N. Jussien

PDF

Symbolic Execution for Software Testing: Three Decades Later. 2013

C. Cadar, K. Sen

ACM

Feedback-directed unit test generation for C/C++ using concolic execution. 2013

CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. 2002

G. Necula, S. McPeak, S. Rahul, W. Weimer

PDF
ACM

Creating Vulnerability Signatures Using Weakest Preconditions. 2007

PathCrawler: Automatic Generation of Path Tests by Combining Static and Dynamic Analysis. 2005

N. Williams, B. Marre, P. Mouy, M. Roger

ACM

Path Feasibility Analysis for String-Manipulating Programs. 2009

Active Property Checking. 2008

P. Godefroid, M. Levin, D. Molnar

PDF
ACM

Hacking Blind. 2014

A. Bittau, A. Belay, A. Mashtizadeh, D. Mazi`eres, D. Boneh

ACM

Vigilante: End-to-End Containment of Internet Worm Epidemics. 2008

Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. 2008

A Decision Procedure for Bit-Vectors and Arrays. 2007

V. Ganesh, D. Dill

Comprehensive multi-platform dynamic program analysis for the Java and Dalvik virtual machines. 2014

Exact and Approximate Probabilistic Symbolic Execution for Nondeterministic Programs. 2014

Demand-Driven Compositional Symbolic Execution. 2008

LCT: An Open Source Concolic Testing Tool for Java Programs. 2011

Test input generation for java containers using state matching. 2006

Статический анализатор Svace для поиска дефектов в исходном коде программ. 2014

В. Иванников, А. Белеванцев, А. Бородин, В. Игнатьев, Д. Журихин, А. Аветисян, М. Леонов

CRAX: software CRash analysis for Automatic eXploit generation

BitBlaze: A New Approach to Computer Security via Binary Analysis. 2008

D. Song, D. Brumley, H. Yin, J. Caballero, I. Jager, M. Kang, Z. Liang, J. Newsome, P. Poosankam, P. Saxena

PDF

Pex: White Box Test Generation for .NET. 2008

N. Tillmann, J. De Halleux

PDF
ACM

Enhancing Symbolic Execution with Built-In Term Rewriting and Constrained Lazy Initialization. 2013

Symbolic Execution with Abstract Subsumption Checking. 2006

Precise Identification of Problems for Structural Test Generation. 2011

Systematic Testing for Control Applications. 2010

Compositional Dynamic Test Generation. 2007

P. Godefroid

PDF
ACM

Exploring Multiple Execution Paths for Malware Analysis. 2007

Analyzing Memory Accesses in x86 Executables. 2004

G. Balakrishnan, T. Reps

Symbolic Execution with Mixed Concrete-Symbolic Solving. 2011

Solving string constraints lazily. 2010

JCHARMING: A Bug Reproduction Approach using Crash Traces and Directed Model Checking. 2015

Collective Assertions. 2011

Mixing type checking and symbolic execution. 2010

Memory Management in the Java HotSpot™ Virtual Machine

Experimental comparison of concolic and random testing for java card applets. 2010

Higher-Order Test Generation. 2011

Поиск ошибок доступа к буферу в программах на языке C/C++

One VM to Rule Them All. 2013

T. Würthinger, C. Wimmer, A. Wöß, L. Stadler, G. Duboscq, C. Humer, G. Richards, D. Simon, M. Wolczko

ACM

Dynamic Test Generation To Find Integer Bugs in x86 Binary Linux Programs. 2009

Symbolic Security Analysis of Ruby-on-Rails Web Applications. 2010

Efficient, transparent, and comprehensive runtime code manipulation. 2004

D. Bruening

PDF

Symbolic Crosschecking of Floating-Point and SIMD Code. 2011

An Orchestrated Survey of Methodologies for Automated Software Test Case Generation. 2013

S. Anand, E. Burke, T. Chen, J. Clark, M. Cohen, W. Grieskamp, M. Harman, M. Harrold, P. Mcminn

PDF
ACM

The Geometry of Innocent Flesh on the Bone: Return-into-libc Without Function Calls (on the x86). 2007

H. Shacham

ACM

Automatically Generating Malicious Disks using Symbolic Execution. 2006

Randomized Instruction Set Emulation. 2005

E. Barrantes, D. Ackley, S. Forrest, D. Stefanović

ACM

CERT

Scalable and scope-bounded software verification in Varvel. 2015

F. ić, G. Balakrishnan, A. Gupta, S. Sankaranarayanan, N. Maeda, T. Imoto, R. Pothengil, M. Hussain

Computational verification of C protocol implementations by symbolic execution. 2012

База данных Common Weakness Enumeration (CWE). 2016

A Decision Procedure for Subset Constraints over Regular Languages. 2009

P. Hooimeijer, W. Weimer

ACM

kb-Anonymity: A Model for Anonymized Behavior-Preserving Test and Debugging Data. 2011

Bogor: an extensible and highly-modular software model checking framework. 2003

Reggae: Automated Test Generation for Programs Using Complex Regular Expressions. 2009

A Static Analyzer for Finding Dynamic Programming Errors. 2000

W. Bush, J. Pincus, D. Sielaff

ACM

JMD: A Hybrid Approach for Detecting Java Malware

PDF

Valgrind: A Framework for Heavyweight Dynamic Binary Instrumentation. 2007

N. Nethercote, J. Seward

PDF
ACM

WAPTEC: whitebox analysis of web applications for parameter tampering exploit construction. 2011

Comprehensive Multi-platform Dynamic Program Analysis for Java and Android

Surgically returning to randomized lib(c). 2009

G. Roglia, L. Martignoni, R. Paleari, D. Bruschi

Statistical Symbolic Execution with Informed Sampling. 2014

PDF

A History of Satisfiability. 2009

J. Franco, J. Martin

PDF

Using Test Case Reduction and Prioritization to Improve Symbolic Execution. 2014

Multi-Prover Verification of Floating-Point Programs. 2010

Определение тьюринг-полноты

Avian. A lightweight alternative to Java

STAR: Stack Trace based Automatic Crash Reproduction via Symbolic Execution. 2015

Make Test-zesti: A Symbolic Execution Solution for Improving Regression Testing. 2012

P. Marinescu, C. Cadar

ACM

Test Input Generation for Programs with Pointers. 2009

Precise pointer reasoning for dynamic test generation. 2009

Data Races vs. Data Race Bugs: Telling the Difference with Portend. 2012

Selecting peers for execution comparison. 2011

Binary Analysis Tools and Binary Code

REIL: A platform-independent intermediate representation of disassembled code for static code analysis. 2009

T. Dullien, S. Porst

eXpress: Guided Path Exploration for Efficient Regression Test Generation. 2011

Bounded Integer Linear Constraint Solving via Lattice Search. 2015

Automatically Identifying Trigger-based Behavior in Malware. 2008

Execution Generated Test Cases: How to Make Systems Code Crash Itself. 2005

PDF

Path Exploration based on Symbolic Output. 2011

MultiSE: multi-path symbolic execution using value summaries. 2015

Avalanche. Применение динамического анализа для генерации входных данных, демонстрирующих критические ошибки и уязвимости в программах. 2010

И. Исаев, Д. Сидоров

PDF

Randomized directed testing (REDIRECT) for Simulink/Stateflow models. 2008

PDF

Bouncer: securing software by blocking bad input. 2007

SAGE: Whitebox Fuzzing for Security Testing. 2012

P. Godefroid, M. Levin, D. Molnar

PDF
ACM

Automated Concolic Testing of Smartphone Apps. 2012

Finding Bugs in Exceptional Situations of JNI Programs. 2009

PDF

Automated Whitebox Fuzz Testing. 2008

P. Godefroid, M. Levin, D. Molnar

PDF

Type-dependence Analysis and Program Transformation for Symbolic Execution. 2007

S. Anand, A. Orso, M. Harrold

PDF
ACM

The Model Checker SPIN. 1997

G. Holzmann

PDF
ACM

Подходы к определению основного места проживания пользователей социальных сетей на основе социального графа

A dynamic marking method for implicit information flow in dynamic taint analysis. 2015

Xuefei Wang, Hengtai Ma, Lisha Jing

ACM

Extended Static Checking for Java. 2002

Fitness-guided path exploration in dynamic symbolic execution. 2009

Finding the Bad in Good Code: Automated Return-Oriented Programming Exploit Discovery. 2009

R. Roemer

Структурный анализ в задаче декомпиляции

PDF

Runtime Exception Detection in Java Programs Using Symbolic Execution. 2013

PDF

Framing Signals – A Return to Portable Shellcode. 2014

E. Bosman, H. Bos

Dynamic Symbolic Execution with Interpolation Based Path Merging. 2016

Integration testing of software product lines using compositional symbolic execution. 2012

Memoise: A tool for memoized symbolic execution. 2013

Z3str3: A String Solver with Theory-aware Branching. 2017

PDF
Arxiv

Unbounded Symbolic Execution for Program Verification. 2011

Dynamic test input generation for database applications. 2007

TRACER: A Symbolic Execution Tool for Verification. 2012

Плагин exploitable для gdb

GKLEE: concolic verification and test generation for GPUs. 2012

How We Get There: A Context-Guided Search Strategy in Concolic Testing. 2014

Path-based Inductive Synthesis for Program Inversion. 2011

Testing MapReduce-style programs. 2011

Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution. 2005

Redundant State Detection for Dynamic Symbolic Execution. 2013

TaintAll. 2016

Grammar-based Whitebox Fuzzing. 2008

P. Godefroid, A. Kiezun, M. Levin

PDF
ACM

Counterexample-Guided Abstraction Refinement. 2000

E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith

Symbolic Robustness Analysis. 2009

Return-oriented Rootkits: Bypassing Kernel Code Integrity Protection Mechanisms. 2009

R. Hund, T. Holz, F. Freiling

ACM

Practical, low-effort verification of real code using under-constrained execution. 2011

Test-Suite Augmentation for Evolving Software. 2008

Privacy-preserving genomic computation through program specialization. 2010

Efficiently Computing Static Single Assignment Form and the Control Dependence Graph. 1991

R. Cytron, J. Ferrante, B. Rosen, M. Wegman, F. Zadeck

PDF
ACM

Generalizing symbolic execution to library classes. 2005

Collaborative Verification and Testing with Explicit Assumptions. 2012

Reliability analysis in symbolic pathfinder. 2013

CVC4. 2011

C. Barrett, C. Conway, M. Deters, L. Hadarean, D. Jovanović, T. King, A. Reynolds, C. Tinelli

ACM

Darwin: an approach for debugging evolving programs. 2009

Extending a Search-Based Test Generator with Adaptive Dynamic Symbolic Execution. 2014

Automatic Partial Loop Summarization in Dynamic Test Generation. 2011

Lazy symbolic execution for test data generation. 2011

A Generic Framework for Symbolic Execution. 2013

Theoretical aspects of compositional symbolic execution. 2011

Test input generation for red-black trees using abstraction. 2005

Is Data Privacy Always Good for Software Testing?. 2010

Automatically Preparing Safe SQL Queries. 2010

Using symbolic evaluation to understand behavior in configurable software systems. 2010

Reverse engineering of binary device drivers with RevNIC. 2010

MATRIX: Maintenance-Oriented Testing Requirements Identifier and Examiner. 2006

Proving Memory Safety of Floating-Point Computations by Combining Static and Dynamic Program Analysis. 2010

Explicating symbolic execution (xSymExe): an evidence-based verification framework. 2013

Automated Software Test Data Generation. 1990

B. Korel

PDF
ACM

NoTamper: Automatic Blackbox Detection of Parameter Tampering Opportunities in Web Applications. 2010

Dowsing for overflows: A guided fuzzer to find buffer boundary violations. 2013

I. Haller, A. Slowinska, M. Neugschwandtner, H. Bos

PDF

Differential symbolic execution. 2008

Selective Symbolic Execution. 2009

Exploiting program dependencies for scalable multiple-path symbolic execution. 2010

Symbolic Security Analysis of Ruby-on-rails Web Applications. 2010

A. Chaudhuri, J. Foster

ACM

Symbolic Optimization with SMT Solvers. 2014

Y. Li, A. Albarghouthi, Z. Kincaid, A. Gurfinkel, M. Chechik

PDF
ACM

Automatic creation of SQL Injection and cross-site scripting attacks. 2009

Input Generation via Decomposition and Re-Stitching: Finding Bugs in Malware. 2010

PDF

Automating mimicry attacks using static binary analysis. 2005

Automatic Formal Verification of MPI-Based Parallel Programs. 2011

ATOM A System for Building Customized Program Analysis Tools. 1994

A. Srivastava, A. Eustace

PDF

Обнаружение ошибок доступа к буферу в программах на языке C/C++ с помощью статического анализа

Finding Trojan Message Vulnerabilities in Distributed Systems. 2014

An empirical investigation into branch coverage for C programs using CUTE and AUSTIN. 2010

Symbolic Testing and the DISSECT Symbolic Evaluation System. 1977

BAP: A Binary Analysis Platform. 2011

D. Brumley, I. Jager, T. Avgerinos, E. Schwartz

PDF

Jalangi: a tool framework for concolic testing, selective record-replay, and dynamic analysis of JavaScript. 2013

Dynamic Test Input Generation for Web Applications. 2008

Synthesizing Parameterized Unit Tests to Detect Object Invariant Violations. 2014

Hey, you, get off of my market: detecting malicious apps in official and alternative android markets.. 2012

Y. Zhou, Z. Wang, W. Zhou, X. Jiang

PDF

Towards Automatic Discovery of Deviations in Binary Implementations with Applications to Error Detection and Fingerprint Generation. 2007

D. Brumley, J. Caballero, Z. Liang, J. Newsome, D. Song

PDF
ACM

Parallel Symbolic Execution for Automated Real-world Software Testing. 2011

S. Bucur, V. Ureche, C. Zamfir, G. Candea

PDF
ACM

Reducing Test Inputs Using Information Partitions. 2009

A Decision Procedure for Bit-vectors and Arrays. 2007

V. Ganesh, D. Dill

PDF
ACM

Scaling symbolic execution using ranged analysis. 2012

Capstone. The Ultimate Disassembler

Deconstructing Dynamic Symbolic Execution. 2015

PDF

Anywhere, any-time binary instrumentation. 2011

A. Bernat, B. Miller

Billions and Billions of Constraints: Whitebox Fuzz Testing in Production. 2013

Symbolic execution with abstraction. 2009

An advanced automatic construction method of ROP. 2015

Y. Ouyang, Q. Wang, J. Peng, J. Zeng

HAMPI: A Solver for String Constraints. 2009

A. Kiezun, V. Ganesh, P. Guo, P. Hooimeijer, M. Ernst

ACM

Dynamic Test Generation with Static Fields and Initializers. 2014

Software Crash Analysis for Automatic Exploit Generation on Binary Programs

MACE: Model-inference-Assisted Concolic Exploration for Protocol and Vulnerability Discovery. 2011

Jinn: Synthesizing Dynamic Bug Detectors for Foreign Language Interfaces. 2010

B. Lee, B. Wiedermann, M. Hirzel, R. Grimm, K. McKinley

PDF
ACM

JReq: Database Queries in Imperative Languages. 2010

SymDroid: Symbolic Execution for Dalvik Bytecode. 2012

J. Jeon, K. Micinski, J. Foster

PDF

Directed Test Generation for Effective Fault Localization. 2010

Bogor/Kiasan: A k-bounded Symbolic Execution for Checking Strong Heap Properties of Open Systems. 2006

QAGen: generating query-aware test databases. 2007

An API for Runtime Code Patching. 2000

B. Buck, J. Hollingsworth

PDF
ACM

The Complexity of Theorem-Proving Procedures. 1971

S. Cook

PDF
ACM

Automatic Generation of Control Flow Hijacking Exploits for Software Vulnerabilities. 2009

S. Heelan

Optimizing Constraint Solving to Better Support Symbolic Execution. 2011

Universal symbolic execution and its application to likely data structure invariant generation. 2008

Automatically Discovering, Reporting and Reproducing Android Application Crashes. 2016

WISE: Automated test generation for worst-case complexity. 2009

Personalized Defect Prediction. 2013

PDF

ThreadSanitizer: Data Race Detection in Practice. 2009

K. Serebryany, T. Iskhodzhanov

PDF
ACM

Symdrive: testing drivers without devices. 2012

Euclide: A Constraint-Based Testing Framework for Critical C Programs. 2009

QEMU, a fast and portable dynamic translator. 2005

Bellard F.

Steering symbolic execution to less traveled paths. 2013

SmacC: A Retargetable Symbolic Execution Engine. 2013

Snugglebug: a powerful approach to weakest preconditions. 2009

Looper: Lightweight Detection of Infinite Loops at Runtime. 2009

SymJS: Automatic Symbolic Testing of JavaScript Web Applications. 2014

G. Li, E. Andreasen, I. Ghosh

PDF
ACM

State Joining and Splitting for the Symbolic Execution of Binaries. 2009

RWset: Attacking Path Explosion in Constraint-Based Test Generation. 2008

Precise interface identification to improve testing and analysis of web applications. 2009

Codesonar for binaries

Input-covering schedules for multithreaded programs. 2013

Heuristics for Scalable Dynamic Test Generation. 2008

Abstract Analysis of Symbolic Executions. 2010

Predictive testing: amplifying the effectiveness of software testing. 2007

Symbiotic: Synergy of instrumentation, slicing, and symbolic execution. 2013

Boosting concolic testing via interpolation. 2013

Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. 2009

R. Brummayer, A. Biere

PDF
ACM

Directed test generation using symbolic grammars. 2007

Saturn: A scalable framework for error detection using Boolean satisfiability. 2007

PDF

A Scalable Distributed Concolic Testing Approach: An Empirical Evaluation. 2012

IntScope: Automatically Detecting Integer Overflow Vulnerability in X86 Binary Using Symbolic Execution. 2009

Dynamic symbolic database application testing. 2010

Dytan: a generic dynamic taint analysis framework. 2007

J. Clause, W. Li, A. Orso

PDF
ACM

Augmented dynamic symbolic execution. 2012

K. Jamrozik, G. Fraser, N. Tillmann, J. De Halleux

Varieties of Static Analyzers: A Comparison with ASTREE. 2007

P. Cousot, R. Cousot, J. Feret, A. Miné, L. Mauborgne, D. Monniaux, X. Rival

Parallel Symbolic Execution for Automated Real-World Software Testing. 2011

Directed Incremental Symbolic Execution. 2011

Bandera: a source-level interface for model checking Java programs. 2000

Symbolic execution of floating-point computations. 2006

The Program Dependence Graph and Its Use in Optimization. 1987

J. Ferrante, K. Ottenstein, J. Warren

PDF
ACM

Q: Exploit Hardening Made Easy. 2011

E. Schwartz, T. Avgerinos, D. Brumley

ACM

Camouflage: Automated Anonymization of Field Data. 2011

The SMT-LIB Standard. 2015

C. Barrett, P. Fontaine, C. Tinelli

Triton: A Dynamic Symbolic Execution Framework. 2015

F. Saudel, J. Salwan

Prototyping Symbolic Execution Engines for Interpreted Languages. 2014

Rubicon: bounded verification of web applications. 2012

Parallel symbolic execution for structural test generation. 2010

Verification of Java Programs Using Symbolic Execution and Invariant Generation. 2004

Eraser: A Dynamic Data Race Detector for Multithreaded Programs. 1997

S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, T. Anderson

PDF
ACM

Panalyst: privacy-aware remote error analysis on commodity software. 2008

S2E: Design, Implementations and Applications. 2012

V. Chipounov, V. Kuznetsov, G. Candea

Combining symbolic execution with model checking to verify parallel numerical programs. 2008

The JVM is Not Observable Enough (and What To Do About It). 2012

PDF

Multi-solver Support in Symbolic Execution. 2013

PDF

Automated Extraction of Failure Reproduction Steps from User Interaction Traces. 2015

Variably interprocedural program analysis for runtime error detection. 2007

Loop invariant symbolic execution for parallel programs. 2012

Finding latent code errors via machine learning over program executions. 2004

Y. Brun, M. Ernst

PDF

Verifying systems rules using rule-directed symbolic execution. 2013

Z3str2: an efficient solver for strings, regular expressions, and length constraints. 2017

Y. Zheng, V. Ganesh, S. Subramanian, O. Tripp, M. Berzish, J. Dolby, X. Zhang

PDF

An SMT-LIB Theory of Binary Floating-Point Arithmetic. 2010

PDF

Compositional may-must program analysis: unleashing the power of alternation. 2010

Analyzing memory accesses in x86 executables.. 2004

G. Balakrishnan, T. Reps

AppIntent: Analyzing Sensitive Data Transmission in Android for Privacy Leakage Detection. 2013

Z. Yang, M. Yang, Y. Zhang, G. Gu, P. Ning, X. Wang

ACM

A survey of new trends in symbolic execution for software testing and analysis. 2009

C. Păsăreanu, W. Visser

DySy: dynamic symbolic execution for invariant inference. 2008

Analyze Crashes to Find Security Vulnerabilities in Your Apps

Sireum/Topi LDP: a lightweight semi-decision procedure for optimizing symbolic execution-based analyses. 2009

Buffer Overflows: Anatomy of an Exploit. 2012

PDF

Hybrid Concolic Testing. 2007

R. Majumdar, K. Sen

PDF
ACM

BitScope: Automatically Dissecting Malicious Binaries. 2007

Calysto: scalable and precise extended static checking. 2008

Path-exploration Lifting: Hi-fi Tests for Lo-fi Emulators. 2012

L. Martignoni, S. McCamant, P. Poosankam, D. Song, P. Maniatis

PDF
ACM

Exploiting Undefined Behaviors for Efficient Symbolic Execution. 2014

A. Sharma

PDF
ACM

CIVL: The Concurrency Intermediate Verification Language. 2015

S. Siegel, M. Zheng, Z. Luo, T. Zirkel, A. Marianiello, J. Edenhofner, M. Dwyer, M. Rogers

PDF
ACM

Symbolic Execution Debugger (SED). 2014

M. Hentschel, R. Bubel, R. hnle

Chaff: Engineering an Efficient SAT Solver. 2001

M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, S. Malik

PDF
ACM

GRASP---a New Search Algorithm for Satisfiability. 1996

J. Silva, K. Sakallah

PDF
ACM

SATO: An Efficient Propositional Prover. 1997

H. Zhang

PDF
ACM

A Computing Procedure for Quantification Theory. 1960

M. Davis, H. Putnam

ACM

jFuzz: A Concolic Whitebox Fuzzer for Java. 2009

K. Jayaraman, D. Harvison, V. Ganesh, A. Kie.zun

PDF

SWEET: Serving the Web by Exploiting Email Tunnels. 2012

A. Houmansadr, W. Zhou, M. Caesar, N. Borisov

PDF
Arxiv

JumpBox -- A Seamless Browser Proxy for Tor Pluggable Transports. 2015

J. Massar, I. Mason, L. Briesemeister, V. Yegneswaran

PDF

CensorSpoofer: Asymmetric Communication Using IP Spoofing for Censorship-resistant Web Browsing. 2012

Q. Wang, X. Gong, G. Nguyen, A. Houmansadr, N. Borisov

PDF
Arxiv
ACM

On the evolution of buffer overflows. 2007

M. Vallentin

SELECT&Mdash;a Formal System for Testing and Debugging Programs by Symbolic Execution. 1975

R. Boyer, B. Elspas, K. Levitt

ACM

Improving Function Coverage with Munch: A Hybrid Fuzzing and Directed Symbolic Execution Approach. 2017

S. Ognawala, T. Hutzelmann, E. Psallida, A. Pretschner

PDF
Arxiv

String Constraints for Verification. 2014

P. Abdulla, M. Atig, Y. Chen, L. k, A. Rezine, P. mmer, J. Stenman

Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic. 2009

S. Jha, R. Limaye, S. Seshia