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: Ball:Thomas
Facilitated 4 volumes:
Ed
Ed
Ed
EdContributed to:
201420142013
20122012
2011
2011201120102010
2010
2009
2008
2008
20082007
2007
200720062006
2006200520052004
2004200420032002
200220022001200120012001
1999199919981998
19971997199719931992Wrote 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.