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 × Cyprus
1 × Estonia
1 × Hungary
2 × France
2 × Germany
3 × USA
4 × United Kingdom
Collaborated with:
D.Kröning P.Liu E.A.Emerson A.Kaiser G.Basler A.Brillout P.Rümmer R.J.Trefler ∅ A.F.Donaldson M.Purandare N.Blanc K.Athanasiou A.Lal M.Leeser S.Mukherjee J.Ramachandran M.Mazzucchi Y.Chebiryak L.Haller J.Ouaknine O.Strichman J.Worrell M.Tautschnig M.Hague C.L.Ong H.Zhao
Talks about:
program (7) symmetri (4) abstract (4) concurr (4) arithmet (3) reduct (3) use (3) quantifi (2) presburg (2) interpol (2)

Person: Thomas Wahl

DBLP DBLP: Wahl:Thomas

Contributed to:

DATE 20142014
TACAS 20122012
CAV 20112011
VMCAI 20112011
CAV 20102010
IJCAR 20102010
TACAS 20102010
CAV 20092009
DATE 20092009
SAT 20092009
VMCAI 20092009
TACAS 20082008
CAV 20072007
TACAS 20052005
IJCAR 20162016
CAV (2) 20192019
PLDI 20182018

Wrote 18 papers:

DATE-2014-LeeserMRW #effectiveness #float #reasoning
Make it real: Effective floating-point reasoning via exact arithmetic (ML, SM, JR, TW), pp. 1–4.
TACAS-2012-BaslerDKKTW #c #contest #named #source code #verification
satabs: A Bit-Precise Verifier for C Programs — (Competition Contribution) (GB, AFD, AK, DK, MT, TW), pp. 552–555.
CAV-2011-DonaldsonKKW #abstraction #concurrent #source code #symmetry
Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs (AFD, AK, DK, TW), pp. 356–371.
CAV-2011-KroeningOSWW #bound #linear #model checking
Linear Completeness Thresholds for Bounded Model Checking (DK, JO, OS, TW, JW), pp. 557–572.
VMCAI-2011-BrilloutKRW #quantifier
Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (AB, DK, PR, TW), pp. 88–102.
CAV-2010-KaiserKW #concurrent #detection #source code
Dynamic Cutoff Detection in Parameterized Concurrent Programs (AK, DK, TW), pp. 645–659.
IJCAR-2010-BrilloutKRW #calculus #quantifier
An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic (AB, DK, PR, TW), pp. 384–399.
TACAS-2010-BaslerHKOWZ #model checking #named
Boom: Taking Boolean Program Model Checking One Step Further (GB, MH, DK, CHLO, TW, HZ), pp. 145–149.
CAV-2009-BaslerMWK #abstraction #concurrent
Symbolic Counter Abstraction for Concurrent Software (GB, MM, TW, DK), pp. 64–78.
DATE-2009-PurandareWK #abstraction #refinement #using
Strengthening properties using abstraction refinement (MP, TW, DK), pp. 1692–1697.
SAT-2009-ChebiryakWKH #agile
Finding Lean Induced Cycles in Binary Hypercubes (YC, TW, DK, LH), pp. 18–31.
VMCAI-2009-TreflerW #architecture #reduction #symmetry
Extending Symmetry Reduction by Exploiting System Architecture (RJT, TW), pp. 320–334.
TACAS-2008-WahlBE #named #symmetry #verification
SVISS: Symbolic Verification of Symmetric Systems (TW, NB, EAE), pp. 459–462.
CAV-2007-Wahl #adaptation #reduction #symmetry
Adaptive Symmetry Reduction (TW), pp. 393–405.
TACAS-2005-EmersonW #reduction #symmetry
Dynamic Symmetry Reduction (EAE, TW), pp. 382–396.
IJCAR-2016-AthanasiouLW #bound #equation #thread #using #verification
Unbounded-Thread Program Verification using Thread-State Equations (KA, PL, TW), pp. 516–531.
CAV-2019-LiuWL #source code #using #verification
Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers (PL, TW, AL), pp. 386–404.
PLDI-2018-LiuW #analysis #bound #concurrent #interprocedural #named #source code
CUBA: interprocedural Context-UnBounded Analysis of concurrent programs (PL, TW), pp. 105–119.
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.