Vijay Ganesh

Proceedings of the 7th SC-Square Workshop co-located with the Federated Logic Conference, 2022

Gas Gauge: A Security Analysis Tool for Smart Contract Out-of-Gas Vulnerabilities.

[BibT_eX]

[DOI]

Proceedings of the 3rd International Conference on Mathematical Research for Blockchain Economy, 2022

A Solver + Gradient Descent Training Algorithm for Deep Neural Networks.

[BibT_eX]

[DOI]

Dhananjay Ashok

Vineel Nagisetty

Christopher Srinivasa

Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, 2022

2021

Complex Golay pairs up to length 28: A search via computer algebra and programmatic SAT.

[BibT_eX]

[DOI]

J. Symb. Comput., 2021

On the Hierarchical Community Structure of Practical SAT Formulas.

[BibT_eX]

[DOI]

CoRR, 2021

MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

Logic Solvers and Machine Learning: The Next Frontier (keynote abstract).

[BibT_eX]

[DOI]

Proceedings of the 6th SC-Square Workshop co-located with the SIAM Conference on Applied Algebraic Geometry, 2021

On the Hierarchical Community Structure of Practical Boolean Formulas.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2021, 2021

BanditFuzz: Fuzzing SMT Solvers with Multi-agent Reinforcement Learning.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods - 24th International Symposium, 2021

Z3str4: A Multi-armed String Solver.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods - 24th International Symposium, 2021

String Theories Involving Regular Membership Predicates: From Practice to Theory and Back.

[BibT_eX]

[DOI]

Proceedings of the Combinatorics on Words - 13th International Conference, 2021

An SMT Solver for Regular Expressions and Linear Arithmetic over String Length.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

Amnesiac Machine Learning.

[BibT_eX]

[DOI]

Laura Graves

Vineel Nagisetty

Proceedings of the Thirty-Fifth AAAI Conference on Artificial Intelligence, 2021

A SAT-based Resolution of Lam's Problem.

[BibT_eX]

[DOI]

Proceedings of the Thirty-Fifth AAAI Conference on Artificial Intelligence, 2021

Logic Guided Genetic Algorithms (Student Abstract).

[BibT_eX]

[DOI]

Dhananjay Ashok

Sebastian Johann Wetzel

Proceedings of the Thirty-Fifth AAAI Conference on Artificial Intelligence, 2021

2020

New Infinite Families of Perfect Quaternion Sequences and Williamson Sequences.

[BibT_eX]

[DOI]

IEEE Trans. Inf. Theory, 2020

Applying computer algebra systems with SAT solvers to the Williamson conjecture.

[BibT_eX]

[DOI]

J. Symb. Comput., 2020

Logic Guided Genetic Algorithms.

[BibT_eX]

[DOI]

Dhananjay Ashok

Sebastian Johann Wetzel

CoRR, 2020

A Length-aware Regular Expression SMT Solver.

[BibT_eX]

[DOI]

CoRR, 2020

LGML: Logic Guided Machine Learning.

[BibT_eX]

[DOI]

CoRR, 2020

Discovering Symmetry Invariants and Conserved Quantities by Interpreting Siamese Neural Networks.

[BibT_eX]

[DOI]

Sebastian Johann Wetzel

CoRR, 2020

LogicGAN: Logic-guided Generative Adversarial Networks.

[BibT_eX]

[DOI]

CoRR, 2020

A nonexistence certificate for projective planes of order ten with weight 15 codewords.

[BibT_eX]

[DOI]

Appl. Algebra Eng. Commun. Comput., 2020

BanditFuzz: A Reinforcement-Learning Based Performance Fuzzer for SMT Solvers.

[BibT_eX]

[DOI]

Federico Mora

Proceedings of the Software Verification - 12th International Conference, 2020

Abstract: MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers.

[BibT_eX]

[DOI]

Proceedings of the 18th International Workshop on Satisfiability Modulo Theories co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), 2020

Abstract: BanditFuzz: A Reinforcement-Learning based Performance Fuzzer for SMT Solvers.

[BibT_eX]

[DOI]

Federico Mora

Proceedings of the 18th International Workshop on Satisfiability Modulo Theories co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), 2020

Community and LBD-Based Clause Sharing Policy for Parallel SAT Solving.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2020, 2020

Towards a Complexity-Theoretic Understanding of Restarts in SAT Solvers.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2020, 2020

Nonexistence Certificates for Ovals in a Projective Plane of Order Ten.

[BibT_eX]

[DOI]

Proceedings of the Combinatorial Algorithms - 31st International Workshop, 2020

Unsatisfiability Proofs for Weight 16 Codewords in Lam's Problem.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, 2020

Online Bayesian Moment Matching based SAT Solver Heuristics.

[BibT_eX]

[DOI]

Proceedings of the 37th International Conference on Machine Learning, 2020

A Machine Learning Based Splitting Heuristic for Divide-and-Conquer Solvers.

[BibT_eX]

[DOI]

Saeed Nejati

Ludovic Le Frioux

Proceedings of the Principles and Practice of Constraint Programming, 2020

LGML: Logic Guided Machine Learning (Student Abstract).

[BibT_eX]

[DOI]

Proceedings of the Thirty-Fourth AAAI Conference on Artificial Intelligence, 2020

On the Unreasonable Effectiveness of SAT Solvers.

[BibT_eX]

[DOI]

Moshe Y. Vardi

Proceedings of the Beyond the Worst-Case Analysis of Algorithms, 2020

2019

SMTIBEA: a hybrid multi-objective optimization algorithm for configuring large constrained software product lines.

[BibT_eX]

[DOI]

Softw. Syst. Model., 2019

An Empirical Investigation of Randomized Defenses against Adversarial Attacks.

[BibT_eX]

[DOI]

Yannik Potdevin

Dirk Nowotka

CoRR, 2019

The SAT+CAS method for combinatorial search with applications to best matrices.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2019

On the Proof Complexity of MCSAT.

[BibT_eX]

[DOI]

Gereon Kremer

Erika Ábrahám

Proceedings of the 4th SC-Square Workshop co-located with the SIAM Conference on Applied Algebraic Geometry, 2019

Accelerated Learning of Predictive Runtime Monitors for Rare Failure.

[BibT_eX]

[DOI]

Reza Babaee

Hari Govind Vediramana Krishnan

Sean Sedwards

Proceedings of the Runtime Verification - 19th International Conference, 2019

Effective Problem Solving Using SAT Solvers.

[BibT_eX]

[DOI]

Proceedings of the Maple in Mathematics Education and Research - Third Maple Conference, 2019

Theory and practice of string solvers (invited talk abstract).

[BibT_eX]

[DOI]

Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis, 2019

MPro: Combining Static and Symbolic Analysis for Scalable Testing of Smart Contract.

[BibT_eX]

[DOI]

Proceedings of the 30th IEEE International Symposium on Software Reliability Engineering, 2019

Interpolating Strong Induction.

[BibT_eX]

[DOI]

Yakir Vizel

Arie Gurfinkel

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

CDCL(Crypto) SAT solvers for cryptanalysis.

[BibT_eX]

[DOI]

Saeed Nejati

Proceedings of the 29th Annual International Conference on Computer Science and Software Engineering, 2019

SAT solvers and computer algebra systems: a powerful combination for mathematics.

[BibT_eX]

[DOI]

Proceedings of the 29th Annual International Conference on Computer Science and Software Engineering, 2019

A SAT+CAS Approach to Finding Good Matrices: New Examples and Counterexamples.

[BibT_eX]

[DOI]

Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence, 2019

2018

Applying Computer Algebra Systems and SAT Solvers to the Williamson Conjecture.

[BibT_eX]

[DOI]

CoRR, 2018

The Satisfiability of Extended Word Equations: The Boundary Between Decidability and Undecidability.

[BibT_eX]

[DOI]

CoRR, 2018

The SAT+CAS paradigm and the Williamson conjecture.

[BibT_eX]

[DOI]

ACM Commun. Comput. Algebra, 2018

Predicting SAT Solver Performance on Heterogeneous Hardware.

[BibT_eX]

[DOI]

Zack Newsham

Sebastian Fischmeister

Proceedings of Pragmatics of SAT 2015, 2018

Machine Learning-Based Restart Policy for CDCL SAT Solvers.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2018, 2018

The Satisfiability of Word Equations: Decidable and Undecidable Theories.

[BibT_eX]

[DOI]

Proceedings of the Reachability Problems - 12th International Conference, 2018

Enumeration of Complex Golay Pairs via Programmatic SAT.

[BibT_eX]

[DOI]

Proceedings of the 2018 ACM on International Symposium on Symbolic and Algebraic Computation, 2018

An Empirical Study of Branching Heuristics through the Lens of Global Learning Rate.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, 2018

Learning-Sensitive Backdoors with Restarts.

[BibT_eX]

[DOI]

Christoph M. Wintersteiger

Ruben Martins

Proceedings of the Principles and Practice of Constraint Programming, 2018

The Effect of Structural Measures and Merges on SAT Solver Performance.

[BibT_eX]

[DOI]

Christoph M. Wintersteiger

Ruben Martins

Jia Hui Liang

Proceedings of the Principles and Practice of Constraint Programming, 2018

Algebraic Fault Attack on SHA Hash Functions Using Programmatic SAT Solvers.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming, 2018

The Proof Complexity of SMT Solvers.

[BibT_eX]

[DOI]

Robert Robere

Antonina Kolokolova

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

StringFuzz: A Fuzzer for String Solvers.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

A SAT+CAS Method for Enumerating Williamson Matrices of Even Order.

[BibT_eX]

[DOI]

Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, 2018

2017

Combining SAT Solvers with Computer Algebra Systems to Verify Combinatorial Conjectures.

[BibT_eX]

[DOI]

J. Autom. Reason., 2017

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

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2017

Relating Complexity-theoretic Parameters with SAT Solver Performance.

[BibT_eX]

[DOI]

Christoph M. Wintersteiger

Ruben Martins

CoRR, 2017

Z3str3: A String Solver with Theory-aware Branching.

[BibT_eX]

[DOI]

Murphy Berzish

Yunhui Zheng

CoRR, 2017

Adaptive Restart and CEGAR-Based Solver for Inverting Cryptographic Hash Functions.

[BibT_eX]

[DOI]

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2017

A Propagation Rate Based Splitting Heuristic for Divide-and-Conquer Solvers.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28, 2017

An Empirical Study of Branching Heuristics Through the Lens of Global Learning Rate.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28, 2017

Preface.

[BibT_eX]

[DOI]

Matthew England

Proceedings of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation co-located with the 42nd International Symposium on Symbolic and Algebraic Computation (ISSAC 2017), 2017

A solver for a theory of string and bit-vectors.

[BibT_eX]

[DOI]

Proceedings of the 39th International Conference on Software Engineering, 2017

Z3str3: A string solver with theory-aware heuristics.

[BibT_eX]

[DOI]

Murphy Berzish

Yunhui Zheng

Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

Reasoning about Probabilistic Defense Mechanisms against Remote Attacks.

[BibT_eX]

[DOI]

Proceedings of the 2017 IEEE European Symposium on Security and Privacy, 2017

SC-square: when Satisfiability Checking and Symbolic Computation join forces.

[BibT_eX]

[DOI]

Proceedings of the ARCADE 2017, 2017

2016

A Solver for a Theory of Strings and Bit-vectors.

[BibT_eX]

[DOI]

CoRR, 2016

Undecidability of a Theory of Strings, Linear Arithmetic over Length, and String-Number Conversion.

[BibT_eX]

[DOI]

Murphy Berzish

CoRR, 2016

Accelerating the General Simplex Procedure for Linear Real Arithmetic via GPUs.

[BibT_eX]

[DOI]

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2016

MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures.

[BibT_eX]

[DOI]

Proceedings of the 1st Workshop on Satisfiability Checking and Symbolic Computation co-located with 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2016), 2016

Learning Rate Based Branching Heuristic for SAT Solvers.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2016, 2016

MATHCHECK: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, 2016

Combining static analysis and targeted symbolic execution for scalable bug-finding in application binaries.

[BibT_eX]

[DOI]

Riyad Parvez

Paul A. S. Ward

Proceedings of the 26th Annual International Conference on Computer Science and Software Engineering, 2016

Manifold: an SMT-based declarative language for electronic and microfluidic design synthesis.

[BibT_eX]

[DOI]

Proceedings of the 26th Annual International Conference on Computer Science and Software Engineering, 2016

Code obfuscation against symbolic execution attacks.

[BibT_eX]

[DOI]

Sebastian Banescu

Christian S. Collberg

Zack Newsham

Alexander Pretschner

Proceedings of the 32nd Annual Conference on Computer Security Applications, 2016

Exponential Recency Weighted Average Branching Heuristic for SAT Solvers.

[BibT_eX]

[DOI]

Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, 2016

2015

Theory and Practice of SAT Solving (Dagstuhl Seminar 15171).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2015

The Meaning of Attack-Resistant Programs.

[BibT_eX]

[DOI]

Sebastian Banescu

Martín Ochoa

CoRR, 2015

SAT-based analysis of large real-world feature models is easy.

[BibT_eX]

[DOI]

Jia Hui (Jimmy) Liang

Venkatesh Raman

Proceedings of the 19th International Conference on Software Product Line, 2015

SATGraf: Visualizing the Evolution of SAT Formula Structure in Solvers.

[BibT_eX]

[DOI]

Sebastian Fischmeister

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2015, 2015

Understanding VSIDS Branching Heuristics in Conflict-Driven Clause-Learning SAT Solvers.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2015

Short Paper: The Meaning of Attack-Resistant Systems.

[BibT_eX]

[DOI]

Sebastian Banescu

Martín Ochoa

Proceedings of the 10th ACM Workshop on Programming Languages and Analysis for Security, 2015

Effective Search-Space Pruning for Solvers of String Equations, Regular Expressions and Length Constraints.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014

Symbolic Execution and Constraint Solving (Dagstuhl Seminar 14442).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2014

Impact of Community Structure on SAT Solver Performance.

[BibT_eX]

[DOI]

Zack Newsham

Sebastian Fischmeister

Gilles Audemard

Laurent Simon

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2014, 2014

2013

Mohawk: Abstraction-Refinement and Bound-Estimation for Verifying Access Control Policies.

[BibT_eX]

[DOI]

Karthick Jayaraman

Mahesh V. Tripunitara

Steve J. Chapin

ACM Trans. Inf. Syst. Secur., 2013

(Un)Decidability Results for Word Equations with Length and Regular Expression Constraints.

[BibT_eX]

[DOI]

CoRR, 2013

Z3-str: a z3-based string solver for web application analysis.

[BibT_eX]

[DOI]

Yunhui Zheng

Xiangyu Zhang

Proceedings of the Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2013

2012

HAMPI: A solver for word equations over strings, regular expressions, and context-free grammars.

[BibT_eX]

[DOI]

ACM Trans. Softw. Eng. Methodol., 2012

STP/HAMPI and Computer Security

[BibT_eX]

[DOI]

CoRR, 2012

Cryptographic Path Hardening: Hiding Vulnerabilities in Software through Cryptography

[BibT_eX]

[DOI]

Michael Carbin

CoRR, 2012

Lynx: A Programmatic SAT Solver for the RNA-Folding Problem.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2012, 2012

Automatic input rectification.

[BibT_eX]

[DOI]

Proceedings of the 34th International Conference on Software Engineering, 2012

Word Equations with Length Constraints: What's Decidable?

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2012

An SMT-based approach to automated configuration.

[BibT_eX]

[DOI]

Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

SMT-LIB Sequences and Regular Expressions.

[BibT_eX]

[DOI]

Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

2011

ARBAC Policy for a Large Multi-National Bank

[BibT_eX]

[DOI]

Karthick Jayaraman

Mahesh V. Tripunitara

Steve J. Chapin

CoRR, 2011

Automatic error finding in access-control policies.

[BibT_eX]

[DOI]

Karthick Jayaraman

Mahesh V. Tripunitara

Steve J. Chapin

Proceedings of the 18th ACM Conference on Computer and Communications Security, 2011

HAMPI: A String Solver for Testing, Analysis and Vulnerability Detection.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

2009

jFuzz: A Concolic Whitebox Fuzzer for Java.

[BibT_eX]

Proceedings of the First NASA Formal Methods Symposium, 2009

HAMPI: a solver for string constraints.

[BibT_eX]

[DOI]

Proceedings of the Eighteenth International Symposium on Software Testing and Analysis, 2009

Taint-based directed whitebox fuzzing.

[BibT_eX]

[DOI]

Tim Leek

Proceedings of the 31st International Conference on Software Engineering, 2009

2008

EXE: Automatically Generating Inputs of Death.

[BibT_eX]

[DOI]

ACM Trans. Inf. Syst. Secur., 2008

2007

Decision procedures for bit-vectors, arrays and integers.

[BibT_eX]

[DOI]

PhD thesis, 2007

A Decision Procedure for Bit-Vectors and Arrays.

[BibT_eX]

[DOI]

David L. Dill

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2003

An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic.

[BibT_eX]

[DOI]

Sergey Berezin

David L. Dill

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2003

2002

Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods.

[BibT_eX]

[DOI]