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 × Canada
1 × Switzerland
2 × China
2 × Cyprus
2 × Germany
2 × Italy
2 × Spain
23 × USA
4 × France
4 × United Kingdom
Collaborated with:
S.K.Rajamani O.Kupferman V.Levin J.R.Larus N.Nagappan F.Xie S.K.Lahiri B.Cook J.Li M.Sagiv G.Yorsh A.Podelski C.Pacheco F.Logozzo D.Leijen T.W.Reps C.McGarvey S.Burckhardt M.Das M.Musuvathi S.Qadeer A.Zeller M.Naik S.Chaki P.Mataga S.Sagiv D.F.Jerding J.T.Stasko G.Ammons P.d.Halleux N.Swamy D.Perelman S.Gulwani D.Grossman M.D.Ernst L.Zhang S.Das R.Majumdar T.D.Millstein D.L.Atkins T.L.Graves A.Mockus C.Sadowski J.Yi E.Bounimova R.Kumar J.Lichtenberg K.E.Coons M.Siff S.Chandra K.Kunchithapadam G.Basler P.A.Nainar I.Neamtiu S.Adams S.Lerner M.Seigle W.Weimer N.Bjørner A.Gember S.Itzhaky A.Karbyshev M.Schapira A.Valadarsky
Talks about:
softwar (11) abstract (10) program (9) analysi (7) test (6) system (5) profil (5) model (5) hardwar (4) automat (4)

Person: Thomas Ball

DBLP DBLP: Ball:Thomas

Facilitated 4 volumes:

POPL 2011Ed
CAV 2006Ed
PLDI 2006Ed
PASTE 1998Ed

Contributed to:

HILT 20142014
PLDI 20142014
PASTE 20132013
OOPSLA 20122012
PLDI 20122012
ASE 20112011
FASE 20112011
OOPSLA 20112011
CAV 20102010
FASE 20102010
TACAS 20102010
MSR 20092009
ISSTA 20082008
OSDI 20082008
TAP 20082008
CAV 20072007
ICSE 20072007
VMCAI 20072007
ICSE 20062006
ISSTA 20062006
LICS 20062006
CAV 20052005
ICSE 20052005
CAV 20042004
IFM 20042004
TACAS 20042004
POPL 20032003
POPL 20022002
SAS 20022002
TACAS 20022002
CAV 20012001
PASTE 20012001
PLDI 20012001
TACAS 20012001
ESEC/FSE 19991999
ICSE 19991999
ISSTA 19981998
POPL 19981998
ESEC/FSE 19971997
ICSE 19971997
PLDI 19971997
PLDI 19931993
POPL 19921992

Wrote 49 papers:

HILT-2014-Ball #compilation #correctness #logic #research #verification
Correctness via compilation to logic: a decade of verification at microsoft research (TB), pp. 69–70.
PLDI-2014-BallBGIKSSV #named #network #source code #towards #verification
VeriCon: towards verifying controller programs in software-defined networks (TB, NB, AG, SI, AK, MS, MS, AV), p. 31.
PASTE-2013-BallHSL #interactive #web
Increasing human-tool interaction via the web (TB, PdH, NS, DL), pp. 49–52.
OOPSLA-2012-LogozzoB #automation #composition #program repair
Modular and verified automatic program repair (FL, TB), pp. 133–146.
PLDI-2012-PerelmanGBG
Type-directed completion of partial expressions (DP, SG, TB, DG), pp. 275–286.
ASE-2011-LiXBLM #formal method #hardware #interface #specification
Formalizing hardware/software interface specifications (JL, FX, TB, VL, CM), pp. 143–152.
FASE-2011-LiXBL #automaton #model checking
Model Checking Büchi Pushdown Systems (JL, FX, TB, VL), pp. 141–155.
OOPSLA-2011-BurckhardtLSYB #incremental #parallel
Two for the price of one: a model for parallel and incremental computation (SB, DL, CS, JY, TB), pp. 427–444.
CAV-2010-BallBLKL #framework #platform #research #verification
The Static Driver Verifier Research Platform (TB, EB, VL, RK, JL), pp. 119–122.
CAV-2010-LiXBL #analysis #automaton #hardware #performance #reachability
Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification (JL, FX, TB, VL), pp. 339–353.
FASE-2010-LiXBLM #approach #hardware
An Automata-Theoretic Approach to Hardware/Software Co-verification (JL, FX, TB, VL, CM), pp. 248–262.
TACAS-2010-BallBCMQ #concurrent #performance #testing
Preemption Sealing for Efficient Concurrency Testing (TB, SB, KEC, MM, SQ), pp. 420–434.
MSR-2009-Ball #research
A brief history of software — from Bell Labs to Microsoft Research (TB).
ISSTA-2008-PachecoLB #dot-net #fault #random testing #testing
Finding errors in .net with feedback-directed random testing (CP, SKL, TB), pp. 87–96.
OSDI-2008-MusuvathiQBBNN #concurrent #source code
Finding and Reproducing Heisenbugs in Concurrent Programs (MM, SQ, TB, GB, PAN, IN), pp. 267–280.
TAP-2008-BallK #testing
Vacuity in Testing (TB, OK), pp. 4–17.
CAV-2007-BallKS #abstraction
Leaping Loops in the Presence of Abstraction (TB, OK, MS), pp. 491–503.
ICSE-2007-PachecoLEB #generative #random testing #testing
Feedback-Directed Random Test Generation (CP, SKL, MDE, TB), pp. 75–84.
VMCAI-2007-BallK #approximate #source code
Better Under-Approximation of Programs by Hiding Variables (TB, OK), pp. 314–328.
ICSE-2006-NagappanBZ #component #metric #mining #predict
Mining metrics to predict component failures (NN, TB, AZ), pp. 452–461.
ISSTA-2006-YorshBS #abstraction #exclamation #proving #testing #theorem proving
Testing, abstraction, theorem proving: better together! (GY, TB, MS), pp. 145–156.
LICS-2006-BallK #abstraction #framework #multi
An Abstraction-Refinement Framework for Multi-Agent Systems (TB, OK), pp. 379–388.
CAV-2005-BallKY #abstraction
Abstraction for Falsification (TB, OK, GY), pp. 67–81.
CAV-2005-LahiriBC #abstraction
Predicate Abstraction via Symbolic Decision Procedures (SKL, TB, BC), pp. 24–38.
ICSE-2005-NagappanB #fault #metric #predict #using
Use of relative code churn measures to predict system defect density (NN, TB), pp. 284–292.
ICSE-2005-NagappanB05a #fault #static analysis #tool support
Static analysis tools as early indicators of pre-release defect density (NN, TB), pp. 580–586.
CAV-2004-BallCLZ #abstraction #automation #named #proving #refinement #theorem proving
Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement (TB, BC, SKL, LZ), pp. 457–461.
IFM-2004-BallCLR #formal method #verification
SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft (TB, BC, VL, SKR), pp. 1–20.
TACAS-2004-BallCDR #abstraction #approximate
Refining Approximations in Software Predicate Abstraction (TB, BC, SD, SKR), pp. 388–403.
TACAS-2004-BallLX #automation #modelling
Automatic Creation of Environment Models via Training (TB, VL, FX), pp. 93–107.
POPL-2003-BallNR #fault
From symptom to cause: localizing errors in counterexample traces (TB, MN, SKR), pp. 97–105.
POPL-2002-BallR #debugging #static analysis
The SLAM project: debugging system software via static analysis (TB, SKR), pp. 1–3.
SAS-2002-AdamsBDLRSW #analysis #data flow #pointer #using
Speeding Up Dataflow Analysis Using Flow-Insensitive Pointer Analysis (SA, TB, MD, SL, SKR, MS, WW), pp. 230–246.
TACAS-2002-BallPR #abstraction #model checking #refinement
Relative Completeness of Abstraction Refinement for Software Model Checking (TB, AP, SKR), pp. 158–172.
CAV-2001-BallR #tool support
The SLAM Toolkit (TB, SKR), pp. 260–264.
PASTE-2001-BallR #data flow #interprocedural #named
Bebop: a path-sensitive interprocedural dataflow engine (TB, SKR), pp. 97–103.
PLDI-2001-BallMMR #abstraction #automation #c #source code
Automatic Predicate Abstraction of C Programs (TB, RM, TDM, SKR), pp. 203–213.
TACAS-2001-BallCR #library #parallel #thread #verification
Parameterized Verification of Multithreaded Software Libraries (TB, SC, SKR), pp. 158–173.
TACAS-2001-BallPR #abstraction #c #model checking #source code
Boolean and Cartesian Abstraction for Model Checking C Programs (TB, AP, SKR), pp. 268–283.
ESEC-FSE-1999-Ball #concept #dynamic analysis
The Concept of Dynamic Analysis (TB), pp. 216–234.
ESEC-FSE-1999-SiffCBKR #c
Coping with Type Casts in C (MS, SC, TB, KK, TWR), pp. 180–198.
ICSE-1999-AtkinsBGM #tool support #using #version control
Using Version Control Data to Evaluate the Impact of Software Tools (DLA, TB, TLG, AM), pp. 324–333.
ISSTA-1998-Ball #analysis #control flow #on the #testing
On the Limit of Control Flow Analysis for Regression Test Selection (TB), pp. 134–142.
POPL-1998-BallMS #profiling
Edge Profiling versus Path Profiling: The Showdown (TB, PM, SS), pp. 134–148.
ESEC-FSE-1997-RepsBDL #maintenance #problem #profiling #using
The Use of Program Profiling for Software Maintenance with Applications to the Year 2000 Problem (TWR, TB, MD, JRL), pp. 432–449.
ICSE-1997-JerdingSB #interactive #visualisation
Visualizing Interactions in Program Executions (DFJ, JTS, TB), pp. 360–370.
PLDI-1997-AmmonsBL #hardware #performance #profiling
Exploiting Hardware Performance Counters with Flow and Context Sensitive Profiling (GA, TB, JRL), pp. 85–96.
PLDI-1993-BallL #branch #for free #predict
Branch Prediction For Free (TB, JRL), pp. 300–313.
POPL-1992-BallL #profiling #source code
Optimally Profiling and Tracing Programs (TB, JRL), pp. 59–70.

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.