BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Austria
1 × China
1 × Portugal
11 × USA
2 × Denmark
2 × France
2 × United Kingdom
3 × Germany
3 × Italy
Collaborated with:
V.Ryvchin S.Chaki D.Kröning A.Pnueli ∅ M.Siegel J.Ouaknine R.Gershman S.A.Seshia A.Gupta Y.Rodeh A.Nadel A.Gurfinkel M.Ryabtsev B.Godlin A.Matsliah M.Rozanov R.E.Bryant O.Meir E.M.Clarke A.Ivrii M.Koifman A.Groce S.Kong O.Grumberg F.Lerda M.Theobald M.Talupur N.Sinha J.H.Kukula T.Wahl J.Worrell B.A.Brady
Talks about:
sat (6) abstract (5) model (5) check (5) increment (4) logic (4) decid (4) bound (4) base (4) translat (3)

Person: Ofer Strichman

DBLP DBLP: Strichman:Ofer

Facilitated 1 volumes:

SAT 2010Ed

Contributed to:

SAT 20152015
SAT 20142014
VMCAI 20132013
SAT 20122012
VMCAI 20122012
CAV 20112011
SAT 20112011
CAV 20092009
DAC 20092009
SAT 20082008
CAV 20072007
SMT 20072008
TACAS 20072007
CAV 20062006
CAV 20052005
POPL 20052005
SAT 20052005
CAV 20042004
FSE 20042004
VMCAI 20042004
VMCAI 20032003
CAV 20022002
CAV 20012001
CAV 20002000
CAV 19991999
FM-Trends 19981998
ICALP 19981998

Wrote 32 papers:

SAT-2015-IvriiRS #incremental #mining #satisfiability
Mining Backbone Literals in Incremental SAT — A New Kind of Incremental Data (AI, VR, OS), pp. 88–103.
SAT-2014-NadelRS #incremental #satisfiability
Ultimately Incremental SAT (AN, VR, OS), pp. 206–218.
VMCAI-2013-ChakiGKS #composition #source code
Compositional Sequentialization of Periodic Programs (SC, AG, SK, OS), pp. 536–554.
SAT-2012-NadelRS #incremental #preprocessor #satisfiability
Preprocessing in Incremental SAT (AN, VR, OS), pp. 256–269.
VMCAI-2012-ChakiGS #concurrent #multi #source code #thread #verification
Regression Verification for Multi-threaded Programs (SC, AG, OS), pp. 119–135.
CAV-2011-KroeningOSWW #bound #linear #model checking
Linear Completeness Thresholds for Bounded Model Checking (DK, JO, OS, TW, JW), pp. 557–572.
SAT-2011-RyvchinS #performance #satisfiability
Faster Extraction of High-Level Minimal Unsatisfiable Cores (VR, OS), pp. 174–187.
CAV-2009-RyabtsevS #c #validation
Translation Validation: From Simulink to C (MR, OS), pp. 696–701.
CAV-2009-Strichman #equivalence #proving #source code #verification
Regression Verification: Proving the Equivalence of Similar Programs (OS), p. 63.
DAC-2009-GodlinS #verification
Regression verification (BG, OS), pp. 466–471.
SAT-2008-RyvchinS
Local Restarts (VR, OS), pp. 271–276.
CAV-2007-MatsliahS #approximate #encryption #model checking #random
Underapproximation for Model-Checking Based on Random Cryptographic Constructions (AM, OS), pp. 339–351.
SMT-2007-RozanovS08 #constraints #generative #logic #similarity #transitive
Generating Minimum Transitivity Constraints in P-time for Deciding Equality Logic (MR, OS), pp. 3–17.
TACAS-2007-BryantKOSSB #abstraction
Deciding Bit-Vector Arithmetic with Abstraction (REB, DK, JO, SAS, OS, BAB), pp. 358–372.
TACAS-2007-ChakiS #reasoning
Optimized L*-Based Assume-Guarantee Reasoning (SC, OS), pp. 276–291.
CAV-2006-GershmanKS #satisfiability
Deriving Small Unsatisfiable Cores with Dominators (RG, MK, OS), pp. 109–122.
CAV-2005-GuptaS #abstraction #bound #model checking #refinement
Abstraction Refinement for Bounded Model Checking (AG, OS), pp. 112–124.
CAV-2005-MeirS #logic #similarity
Yet Another Decision Procedure for Equality Logic (OM, OS), pp. 307–320.
POPL-2005-GrumbergLST #approximate #multi
Proof-guided underapproximation-widening for multi-process systems (OG, FL, OS, MT), pp. 122–131.
SAT-2005-GershmanS #effectiveness #preprocessor
Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas (RG, OS), pp. 423–429.
CAV-2004-KroeningOSS #satisfiability
Abstraction-Based Satisfiability Solving of Presburger Arithmetic (DK, JO, SAS, OS), pp. 308–320.
CAV-2004-TalupurSSP #logic
Range Allocation for Separation Logic (MT, NS, OS, AP), pp. 148–161.
FSE-2004-ChakiGS
Explaining abstract counterexamples (SC, AG, OS), pp. 73–82.
VMCAI-2004-ClarkeKOS #bound #complexity #model checking
Completeness and Complexity of Bounded Model Checking (EMC, DK, JO, OS), pp. 85–96.
VMCAI-2003-KroeningS #performance
Efficient Computation of Recurrence Diameters (DK, OS), pp. 298–309.
CAV-2002-ClarkeGKS #abstraction #machine learning #satisfiability #using
SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques (EMC, AG, JHK, OS), pp. 265–279.
CAV-2002-StrichmanSB #satisfiability
Deciding Separation Formulas with SAT (OS, SAS, REB), pp. 209–222.
CAV-2001-RodehS #equivalence #finite #logic
Finite Instantiations in Equivalence Logic with Uninterpreted Functions (YR, OS), pp. 144–154.
CAV-2000-Shtrichman #bound #model checking #satisfiability
Tuning SAT Checkers for Bounded Model Checking (OS), pp. 480–494.
CAV-1999-PnueliRSS #similarity
Deciding Equality Formulas by Small Domains Instantiations (AP, YR, OS, MS), pp. 455–469.
FM-1998-PnueliSS #validation
Translation Validation: From DC+ to C* (AP, OS, MS), pp. 137–150.
ICALP-1998-PnueliSS #validation
Translation Validation for Synchronous Languages (AP, OS, MS), pp. 235–246.
Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.