|
Conference version
|
Journal version
|
Presentation
|
|
Combining
BMC and Complementary Approximate Reachability to Accelerate Bug-Finding.
Proc. of the 41 international conference on computer-aided design (ICCAD’22).
Together with Xiaoyu Zhang, Shengping Xiao, Jianwen Li and Geguang Pu.
|
|
Presentation
|
|
Exploiting
Isomorphic Subgraphs in SAT. Proc. of the 21th conference on
Formal Methods in Computer-Aided Design (FMCAD’21). Together with Alexander
Ivrii.
|
|
Presentation
|
|
Synthesizing
Reactive Systems Using Robustness and Recovery Specifications. Proc. of
the 19th conference on Formal Methods in Computer-Aided Design
(FMCAD’19). Together with Roderick Bloem, Hana Chockler and Masoud Ebrahimi.
|
|
Presentation
|
|
Optimal
algorithm portfolios for computationally hard real-time problems. Proc. of Data-Science meets Optimization (DSO’19), an
IJCAI’19 workshop. Together with Yair Nof.
|
Optimal
algorithm portfolios for computationally
hard
real-time problems. Annals of Mathematics and Artificial
Intelligence (2020). Together with Yair Nof.
|
Presentation
|
|
|
Forward
to the special issue on program equivalence, Formal Methods in Systems
Design.
|
|
|
|
Near-Optimal Course
Scheduling at the Technion.
Interfaces, Volume 47 Issue 6, November-December 2017, pp. 537-554. Available
online also from https://pubsonline.informs.org/doi/full/10.1287/inte.2017.0920
|
|
|
The impact of Entropy and
Solution Density on selected SAT heuristics. In CoRR
arXiv:1706.05637. Together with Dor Cohen.
|
The Impact of
Entropy and Solution Density on
Selected
SAT Heuristics,
Entropy 2018, 20, 713; Together with Dor Cohen.
|
presentation
|
|
Decision-Making with Cross-Entropy
for Self-Adaptation. Proc. of 12th international symposium on
software engineering for adaptive and self-managing systems (SEAMS’17).
Together with Gabriel A. Moreno, Sagar Chaki and Radislav
Vaisman.
|
|
Presentation
|
|
Synthesizing Non-Vacuous Systems
Proc. of 18th Conference on Verification, Model Checking, and Abstract
Interpretation – VMCAI 2017. Together with Roderick Bloem, Hana Chockler and
Masoud Ebrahimi.
|
Vacuity
in Synthesis, Formal Methods in Systems Design, 2021. Together with Roderick Bloem, Hana Chockler and Masoud
Ebrahimi.
|
Presentation
|
|
Regression
Verification for unbalanced recursive functions Proc. of 21st International Symposium on
Formal Methods (FM’16). Together with Maor Veitsman.
|
|
Presentation
|
|
Minimal
unsatisfiable core extraction for SMT. Proc. of the 16th conference on Formal
Methods in Computer Aided Design (FMCAD’16). Together with Ofer Guthman and
Anna Trostanetski.
|
|
Presentation
|
|
Mining
Backbone Literals in Incremental SAT -a new kind of incremental data. Proc. of the 18th International conference on theory and applications of
satisfiability testing (SAT’15), pages 88-103. Together with
Alexander Ivrii and Vadim Ryvchin.
|
|
Presentation
(presentation in pdf)
|
|
Learning
the Language of Error Proc. of the 13th International Symposium on Automated
Technology for Verification and Analysis (ATVA’15). Together with Martin Chapman, Hana Chockler, Pascal Kesseli, Daniel
Kroening and Michael Tautschnig. Please read this note.
|
Learning
the language of software errors Journal of Artificial Intelligence
Research (JAIR) 67 (pp 881 – 903), 2020. Together with Hana Chockler, Pascal
Kesseli, and Daniel Kroening.
(This article contains the novel technique of ‘Lazy learning’).
|
Presentation
|
|
Learning
general constraints in CSP Proc. of The 12th International Conference on
Integration of Artificial Intelligence (AI) and Operations Research (OR)
techniques in Constraint Programming (CPAIOR 2015). Together with Michael Veksler.
|
Learning
general constraints in CSP Journal of Artificial Intelligence 238
(2016) 135-153. Together with Michael Veksler.
|
|
|
|
Model Counting
of Monotone CNF Formulas with
Spectra INFORMS Journal on Computing 27(2). Together with Radislav Vaisman and Ilya Gertsbakh,
2015.
|
|
|
Ultimately
Incremental SAT Proc. of the 17th International conference on theory and applications of
satisfiability testing (SAT’14). Together with Alexander Nadel and
Vadim Ryvchin.
|
|
Presentation
|
|
Verifying
Periodic Programs with Priority Inheritance Locks Proc. of
the 13th
conference on Formal Methods in Computer Aided Design (FMCAD’13).
Together with Sagar Chaki and Arie Gurfinkel.
|
|
Presentation
|
|
Efficient
MUS extraction with Resolution Proc. of the 13th conference
on Formal Methods in Computer Aided Design (FMCAD’13). Together with Vadim
Ryvchin and Alexander Nadel. Please read the note.
|
Accelerated
Deletion-based Extraction of Minimal
Unsatisfiable
Cores Journal on Satisfiability, Boolean
Modeling and Computation (JSAT) 9 (2014), pages 27-51. Together
with
Alex Nadel and Vadim Ryvchin.
|
Presentation
|
|
A New Class of Lineage Expressions over
Probabilistic Databases computable in P-time. Proc. Of the7th International
conference on Scalable Uncertainty Management (SUM 2013). Together with Batya Kenig and Avigdor Gal.
|
|
Presentation
|
|
Compositional
Sequentialization of Periodic Programs. Proc. of the
14th International
Conference on Verification,
Model Checking, and Abstract Interpretation (VMCAI’13). Together
with Sagar Chaki, Arie Gurfinkel and Soonho Kong.
|
|
Presentation
|
|
Proving mutual
termination of programs. Proc. of the
eighth Haifa Verification Conference (HVC’12). Together with Dima
Elenbogen and Shmuel Katz.
|
Proving
Mutual Termination. Formal
Methods in Systems Design, Vol 47 issue 2 (2015), pages 204-229. Together with
Dima Elenbogen and Shmuel Katz. You can also get it here via Springerג€™s
online-first.
|
Presentation
|
|
Preprocessing
in Incremental SAT. Proc. of the 15th International conference on theory and applications of
satisfiability testing (SAT’12). Together with Alexander Nadel and
Vadim Ryvchin.
|
|
Presentation
|
|
Regression
Verification for Multi-Threaded Programs. Proc. of 13th International Conference on Verification, Model Checking, and
Abstract Interpretation (VMCAI’12). Together with Sagar Chaki and Arie
Gurfinkel. See also the full
version.
|
Regression
Verification for Multi-Threaded Programs (with extensions to locks and
dynamic thread creation)
Formal Methods in Systems Design vol 47, no 3, pages 287-301. Available also through here via
online-first. Together with Sagar Chaki and Arie Gurfinkel.
|
Presentation
(vsse talk)
|
|
Time-bounded
analysis of real-time systems. Proc. of 11th Formal Methods in Computer Aided Design (FMCAD’11). Together with Sagar Chaki and Arie
Gurfinkel.
|
|
Presentation
|
|
|
A
probabilistic analysis of coverage methods. in ACM Transactions on
Design Automation of Electronic Systems (ACM TDAES), Vol 16, No 4, article 38.
Together with Laurent Fourier, Avi Ziv, and Ekaterina Kutsy.
|
|
|
Linear
Completeness Thresholds for Bounded Model Checking. Proc. of Computer-Aided Verification (CAV’11). Together with Daniel Kroening, Joel
Ouaknine, Thomas Wahl, and James Worrell.
|
|
Presentation
|
|
Faster
Extraction of High-Level Minimal Unsatisfiable Cores. Proc. of Theory and applications of satisfiability testing (SAT’11). Pages 174 – 187. Together with Vadim
Ryvchin. See the HHLMUC
page.
|
(see above: Accelerated deletion-based extraction of
minimal unsatisfiable cores / JSAT /2014)
|
Presentation
|
|
Variants
of LTL query checking. Proc. of Haifa
Verification Conference (HVC’10). Pages 76 – 92. Together with Hana Chockler and Arie Gurfinkel.
|
|
Presentation
|
|
A proof
producing CSP solver. Proc. of the 24th conference of the Association for the Advancement of Artificial Intelligence
(AAAI’10). Together
with Michael Veksler.
|
|
Presentation
(cspsat talk)
(PTHG-20
talk)
|
|
Decision
Diagrams for Linear Arithmetic. Proc. of 9th Formal Methods
in Computer Aided Design (FMCAD’09). Pages 53 – 60. Together with Sagar Chaki and Arie Gurfinkel.
|
|
Presentation
|
|
Regression
Verification. Proc. of 46th Design Automation Conference
(DAC’09). Pages 466 – 471. Together with Benny Godlin.
|
Regression verification:
Proving the equivalence of similar programs. Software Testing, Verification and Reliability, 23(3) 241
-258, 2013. Together with Benny Godliln.
|
Presentation
|
|
Translation
Validation: From Simulink to C. Proc. of Computer
Aided Verification (CAV’09). Together with Michael Ryabtsev.
|
|
Presentation
|
|
|
A framework
for satisfiability modulo theories–
Formal Aspects
of Computing Journal. Vol. 21 (5) 2009, pages 485 –
494. Together with Daniel Kroening.
|
|
|
Easier
and more informative vacuity checks Proc. of the Fifth ACM-IEEE International
Conference on Formal Methods and Models for Codesign (MEMOCODE’2007). Together with
Hana Chockler.
|
Before and
after vacuity.
Formal Methods
in Systems Design. Vol. 34 (1) 2009, pages 37 –
58. Together with Hana Chockler.
|
Presentation
|
|
HaifaSat: a new robust SAT solver Proc. of Haifa Verification Conference (HVC’05).
LNCS vol. 3875, pages 76 – 89 . Together with
Roman Gershman.
|
HaifaSat: a SAT solver based on an abstrction/refinement
model. In JSAT – Journal on Satisfiability, Boolean Modeling and
Computation. Vol.
6 (2008), pages 33 – 51. Together with Roman Gerhman.
|
Presentation
|
|
Beyond
Vacuity: Towards the Strongest Passing Formula.
Proc. of the
8th conference on Formal Methods in Computer Aided Design (FMCAD’08).
Pages 188
– 195. Together with Hana Chockler and Arie Gurfinkel.
|
Beyond
Vacuity: Towards the strongest passing formula.
In Formal
Methods in systems Design. Volume 43, Issue 3 (2013), Page 552-571.
Together with
Hana Chockler and Arie Gurfinkel.
|
Presentation
|
|
Linear-time
Reductions of Resolution Proofs. Proc. of Haifa
Verification Conference (HVC 2008). LNCS 5394, pages 114 – 128. Together
with Omer Bar-Ilan, Oded Fuhrmann, Shlomo Hoory and Ohad Shacham.
|
Reducing
the Size of Resolution Proofs in Linear
Time. Journal on Software Tools and Technology Transfer (STTT),
vol 13, issue 3, page 263, 2011. Together with Omer Bar-Ilan, Oded
Fuhrmann, Shlomo Hoory and Ohad Shacham.
|
Presentation
|
|
A
Theory-Based Decision Heuristic for DPLL(T). Proc. of the 8th
conference on Formal Methods in Computer Aided Design (FMCAD’08). Pages
93 –
100. Together with Dan Goldwasser and Shai Fine.
|
|
Presentation
|
|
Optimized
L*-based Assume-Guarantee Reasoning Proc. of the Thirteenth International
Conference on Tools
and Algorithms for the Construction and Analysis of Systems (TACAS’07). Together with
Sagar Chaki.
|
Three
optimizations for Assume-Guarantee reasoning with L*. Formal Methods
in Systems Design, Vol. 32, number 3, pages 267 – 284, 2008. Together
with Sagar Chaki.
|
Presentation
|
|
Deciding
Bit-Vector Arithmetic with Abstraction Proc. of the Thirteenth International
Conference on
Tools and Algorithms for the Construction and Analysis of Systems (TACAS’07). Together with Randal E.
Bryant, Daniel Kroening, Joel Ouaknine, Sanjit Seshia and Bryan Brady.
|
An
Abstraction-Based Decision Procedure for Bit-Vector Arithmetic. Software
Tools and Technology Transfer (STTT) Vol. 11, pages 95 – 104 (2009).
Together with Randal E. Bryant, Daniel Kroening, Joel Ouaknine, Sanjit Seshia
and Bryan Brady.
|
Presentation
|
|
Inference
Rules for Proving the Equivalence of
Recursive
Procedures. (not peer-reviewed) Published in LNCS 6200: Time
for verification – essays in memory of Amir Pnueli.
Together with Benny Godlin.
|
Inference
rules for proving the equivalence of recursive procedures. ACTA
Informatica 45(6) pages 403 – 439, 2008. Together with Benny Godlin.
|
Presentation
|
|
Local restarts.
Proc. of the eleventh International Conference on Theory and Applications
of Satisfiability Testing (SAT’08), LNCS
4996, pages 271 – 276. Together with Vadim Ryvchin.
|
Local restarts
in SAT. In Constraint Programming Letters (CPL), Vol.
4, pages 3 – 13, 2008. Together with Vadim Ryvchin.
|
Presentation
|
|
Deriving small
unsatisfiable cores with dominators Proc. of the 18th International Conference on Computer Aided
Verification (CAV’06). Together with Roman Gershman and Maya
Koifman.
|
An
approach for extracting an unsatisfiable core. Formal Methods in
Systems Design, Vol. 33, pages 1 – 27, 2008. First published online in
SpringerLink on March 2007. Together with Roman Gershman and Maya Koifman.
|
Presentation
|
|
Generating
minimum transitivity constraints in P-time for deciding equality logic. Proc.
of Satisfiability Modulo Theoies
(SMT’07). Together
with Mirron Rozanov. (Vol. 198, issue 2, pages 3 – 17 of Electronic Notes
in Theoretical Computer Science (ENTCS)).
|
|
Presentation
|
|
Underapproximation
for Model-Checking Based on Random Cryptographic Constructions Proc. of the 19th International
Conference on Computer Aided Verification (CAV’07). LNCS 4590
pages 339
– 351. Together with Arie Matsliah.
|
Underapproximation
for Model-Checking Based on Universal Circuits. Information and Computation 208(4), April
2010, pages 315 – 326. Together with Arie Matsliah. (Also available from ScienceDirect) .
|
Presentation
|
|
Finite
Instantiations in Equivalence Logic with Uninterpreted Functions Proc. of the 13th
International Conference on Computer Aided Verification (CAV’01), vol. 2102 of Lecture Notes in
Computer Science, pages 144 – 154, Paris, France, July 2001. Together
with Yoav Rodeh.
|
Building small
equality graphs for deciding Equality Logic with Uninterpreted
Functions Information
and Computation 204 (2006), pages 26 – 59. Together with Yoav Rodeh.
|
|
|
Explaining
Abstract Counterexamples Foundations
of Software Engineering (SIGSOFT – FSE12), pages 73 – 82, Newport Beach, California,
Oct-Nov 2004. Together with S. Chaki and A.
Groce.
|
Error
Explanation with Distance Metrics Intl. Journal on Software Tools for Technology Transfer
(STTT), Vol. 8(3), pages 229 – 247, June 2006. (also available online from https://dx.doi.org/10.1007/s10009-005-0202-0)
Together with A. Groce, S. Chaki and D. Kroening.
|
|
|
Regression
Verification – a practical way to verify programs VSTTE: Verified Software: theories, tools, experiments.
LNCS 4171. Together
with Benny Godlin.
|
|
|
|
Reduced
Functional Consistency of Uninterpreted Functions. Pragmatics of Decision
Procedures for Automated Reasoning (PDPAR’05), July 2005. ENTCS 898
(Vol.144, issue 2). (also available from
Science-Direct, see here). Together
with Amir Pnueli.
|
|
Presentation
|
|
Cost-Effective
Hyper-Resolution for Preprocessing CNF Formulas (full version) Eighth
International Conference on Theory and Applications of Satisfiability Testing
(SAT’05). LNCS vol.
3569, pages 423 – 429. Together with Roman Gershman.
|
|
|
|
Yet another
Decision Procedure for Equality Logic
Proc. of the 17th International Conference on Computer Aided Verification
(CAV’05), LNCS vol.
3576, pages 307-320. Together with Orly Meir. You might-as-well read the full
version or even Orly‘s thesis.
See the technical
report for a solution
to the problem posed in this publication. Also, please read this note.
|
|
Presentation
|
|
Abstraction
Refinement for Bounded Model Checking Proc. of the 17th International Conference on Computer
Aided Verification (CAV’05), LNCS
vol. 3576, pages 112 – 124. Together with Anubhav Gupta.
|
|
Presentation
|
|
Proof-guided
underapproximation-widening for multi-process systems Proc. of the 32nd ACM SIGPLAN-SIGACT symposium on
Principles of programming languages (POPL’05) pages 122 –
131, 2005. Together with Orna Grumberg, Flavio Lerda and Michael Theobald.
|
|
|
|
Completeness
and Complexity of Bounded Model-Checking Proc. of the Fifth International Conference on
Verification, Model Checking and Abstract Interpretation (VMCAI 2004). Together with E.
Clarke, D. Kroening and J. Ouaknine.
|
Computational
Challenges in Bounded Model Checking Intl. Journal on Software Tools for Technology
Transfer (STTT) Vol.7(2),
pages 174-183, Apr 2005. Together with E. Clarke, D. Kroening and J.
Ouaknine.
|
Presentation
|
|
Range
Allocation for Separation Logic Proc.
of the 16th International Conference on Computer Aided Verification (CAV
2004). Together with M. Talupur, N. Sinha and A. Pnueli.
|
|
|
|
SAT based
Abstraction-Refinement using ILP and Machine Learning Techniques Proc. of the 14th
International Conference on Computer Aided Verification, 2002 (CAV’02), Copenhagen, Denmark, July 2002.
Together with E. Clarke, A. Gupta and J. Kukula.
|
SAT based
counterexample-guided abstraction-refinement Transactions on Computer Aided
Design (TCAD), Vol.23(7), July 2004, pages 1113 – 1123. Together with A.
Gupta and E. Clarke.
|
|
|
Predicate
Abstraction with Minimum Predicates Proc.
of the 12th Advanced Research Working Conference on Correct Hardware Design
and Verification Methods (CHARME’03), Oct 2003. Together with S.
Chaki, E. Clarke and A. Groce.
|
Efficient Verification
of Sequential and Concurrent C programs Journal
on Formal Methods in Systems Design (FMSD). Vol. 25 (2-3),
Sep – Nov 2004, pages 129-166. Together with S. Chaki, E. Clarke, A. Groce,
J. Ouaknine and K. Yorav.
|
Presentation
|
|
Abstraction-Based
Satisfiability Solving of Presburger
Arithmetic Proc.
of the 16th International Conference on Computer Aided Verification (CAV
2004). Together with D. Kroening, J. Ouaknine and S. Seshia.
|
|
|
|
Pruning
techniques for the SAT-based Bounded Model Checking Problem Proc. of the 11th Advanced
Research Working Conference on Correct Hardware Design and Verification
Methods (CHARME’01), vol.
2144 of Lecture Notes in Computer Science, pages 58 – 70,
Livingston, Scotland, Sep. 2001.
|
Accelerating
Bounded Model Checking of Safety Formulas. Formal Methods in System Design, Vol. 24(1), Jan
2004, pages 5-24. (This article combines and extends the articles that
appeared in CAV’00 and CHARME’01. See below).
|
Presentation
|
|
Tuning SAT
checkers for Bounded Model-Checking Proc.
of the 12th International Conference on Computer Aided Verification,
2000 (CAV’00). The
associated technical report can be downloaded from here (word file) or viewed from here (html). The Benchmark files can be
downloaded from SATLIB.
|
(see above: FMSD 24 (1), 2004).
|
Presentation
|
|
Efficient
Computation of Recurrence Diameter Proc. of the Fourth International Conference on
Verification, Model Checking and Abstract Interpretation (VMCAI 2003), Jan 2003.
Together with D. Kroening.
|
|
|
|
|
Bounded
Model Checking (Book chapter) Advances in Computers
#58. Published
in 2003. Together with A. Biere, A. Cimatti, E. Clarke and Y. Zhu. Please
read this note.
|
|
|
Deciding
Equality Formulas by Small Domains Instantiations Proc. of the 11th International Conference
Computer Aided Verification, 1999 (CAV’99). Together with A. Pnueli,
Y. Rodeh and M. Siegel.
|
The Small
Model Property: How small can it be? Information and Computation, Vol.
178(1), Oct 2002, pages 279-293. Together with A. Pnueli,
Y. Rodeh and M. Siegel.
|
Presentation
|
|
On Solving Presburger and Linear Arithmetic with SAT Proc. of Formal Methods in
Computer-Aided Design (FMCAD’02). (Please read the note).
|
|
Presentation
|
|
A Failed
Attempt to Optimize Variable Ordering with Tools for Constraint Solving Proc. of the First
International Workshop on Constraints in Formal Verification (CFV’02), Ithaca,
New-York, Sep 2002. Together with E. Clarke.
|
|
|
|
Deciding
separation formulas with SAT Proc.
of the 14th International Conference on Computer Aided Verification, 2002 (CAV’02). Together with S.
Seshia and R. Bryant.
|
|
Presentation
|
|
SAFEAIR:
Advanced Design Tools for Aircraft Systems and Airborne Software Intl. conference on Dependable systems and networks
(DSN’01). June
2001, Goteborg, Sweden.
Together with P.Baufreton,
F.Dupont, T.Lesergent, M.Segelken, H.Brinkmann and K.Winkelmann.
|
|
|
|
Range
Allocation for Equivalence Logic Proc.
of the 21st conference on Foundations of Software Technology and Theoretical
Computer Science (FSTTCS’01), Bangalore,
India,
December 2001. Together with Yoav Rodeh and Amir Pnueli.
|
|
|
|
|
Translation
Validation: from SIGNAL to C (A Book chapter) In Correct System
Design: Recent Insights and Advances, an LNCS State-of-the-Art Survey, Vol. 1710, pages 231-255,
1999. Together with A. Pnueli and M. Siegel.
|
|
|
The Code
Validation Tool (CVT) – Automatic verification of code generated from
synchronous languages Proc.
of the intl. workshop of Software Tools for Technology Transfer (STTT’98). Together with A. Pnueli
and M. Siegel.
|
The
Code Validation Tool (CVT) – Automatic verification of a compilation process Intl. Journal on Software
Tools for Technology Transfer (STTT), Vol. 2(2), pages 192 –
201, 1998. Together with A. Pnueli and M. Siegel.
|
|
|
Translation
Validation: From DC+ to C Proc. of
the International Workshop on Current Trends in Applied Formal Method:
Applied Formal Methods, Lecture
Notes in Computer Science Vol. 1641, pages 137 – 150, 1998. Together
with A. Pnueli and M. Siegel.
|
|
|
|
Translation
Validation for Synchronous Languages Proc.
of the 25th International Colloquium on Automata, Languages, and Programming
(ICALP’98). Together
with A. Pnueli and M. Siegel.
|
|
|
