Travelled to:1 × China
1 × Estonia
1 × Finland
1 × Portugal
1 × Serbia
2 × Italy
3 × United Kingdom
8 × USA
Collaborated with:S.Falke F.Merz H.Post M.Iser S.Kottler M.Kaufmann T.Jussila A.Biere E.Dieringer ∅ T.Gorges T.Balyo P.Sanders N.Manthey M.Taghdiri D.Kapur W.Blochinger W.Küchlin R.Bündgen J.Walter A.Kaiser T.Kropf D.Kröning C.M.Wintersteiger
Talks about:sat (8) model (6) bound (6) check (4) use (4) checker (3) llbmc (3) intermedi (2) implement (2) contribut (2)
Person: Carsten Sinz
DBLP: Sinz:Carsten
Facilitated 1 volumes:
EdContributed to:
2015
20132013
2013
20122012
2011
2009
20092009200820082007200620052001
20001996Wrote 22 papers:
- SAT-2015-BalyoSS #named #parallel #satisfiability
- HordeSat: A Massively Parallel Portfolio SAT Solver (TB, PS, CS), pp. 156–172.
- SAT-2015-IserMS #recognition
- Recognition of Nested Gates in CNF Formulas (MI, NM, CS), pp. 255–271.
- ASE-2013-FalkeMS #bound #model checking
- The bounded model checker LLBMC (SF, FM, CS), pp. 706–709.
- SAT-2013-IserST #modelling #satisfiability
- Minimizing Models for Tseitin-Encoded SAT Instances (MI, CS, MT), pp. 224–232.
- TACAS-2013-FalkeMS #bound #c #contest #model checking #named #source code #using
- LLBMC: Improved Bounded Model Checking of C Programs Using LLVM — (Competition Contribution) (SF, FM, CS), pp. 623–626.
- SMT-2012-FalkeSM #array #formal method #set
- A Theory of Arrays with set and copy Operations (SF, CS, FM), pp. 98–108.
- TACAS-2012-SinzMF #bound #contest #model checking #named #representation
- LLBMC: A Bounded Model Checker for LLVM’s Intermediate Representation — (Competition Contribution) (CS, FM, SF), pp. 542–544.
- RTA-2011-FalkeKS #analysis #c #compilation #source code #termination #using
- Termination Analysis of C Programs Using Compiler Intermediate Languages (SF, DK, CS), pp. 41–50.
- ICST-2009-PostS #bound #equivalence #functional #implementation #model checking #proving #using
- Proving Functional Equivalence of Two AES Implementations Using Bounded Model Checking (HP, CS), pp. 31–40.
- RE-2009-PostSMGK #functional #requirements #verification
- Linking Functional Requirements and Software Verification (HP, CS, FM, TG, TK), pp. 295–302.
- SAT-2009-SinzI #heuristic #problem
- Problem-Sensitive Restart Heuristics for the DPLL Procedure (CS, MI), pp. 356–362.
- ASE-2008-PostS #verification
- Configuration Lifting: Verification meets Software Configuration (HP, CS), pp. 347–350.
- ASE-2008-PostSKG #abstract interpretation #bound #model checking
- Reducing False Positives by Combining Abstract Interpretation and Bounded Model Checking (HP, CS, AK, TG), pp. 188–197.
- SAT-2008-KottlerKS
- Computation of Renameable Horn Backdoors (SK, MK, CS), pp. 154–160.
- SAT-2008-KottlerKS08a #bound #np-hard #satisfiability #subclass #using
- A New Bound for an NP-Hard Subclass of 3-SAT Using Backdoors (SK, MK, CS), pp. 161–167.
- SAT-2007-JussilaBSKW #proving #towards
- A First Step Towards a Unified Proof Checker for QBF (TJ, AB, CS, DK, CMW), pp. 201–214.
- SAT-2006-JussilaSB #proving #quantifier #satisfiability
- Extended Resolution Proofs for Symbolic SAT Solving with Quantification (TJ, CS, AB), pp. 54–60.
- SAT-2005-SinzD #named #satisfiability #visualisation
- DPvis — A Tool to Visualize the Structure of SAT Instances (CS, EMD), pp. 257–268.
- SAT-2001-SinzBK #implementation #named #parallel
- PaSAT — Parallel SAT-Checking with Lemma Exchange: Implementation and Applications (CS, WB, WK), pp. 205–216.
- CADE-2000-Sinz #algebra #automation #proving #theorem proving
- System Description: ARA — An Automatic Theorem Prover for Relation Algebras (CS), pp. 177–182.
- RTA-1996-BundgenSW
- ReDuX 1.5: New Facets of Rewriting (RB, CS, JW), pp. 412–415.