Travelled to:1 × Austria
1 × China
1 × Denmark
1 × Hungary
1 × India
1 × Russia
1 × Spain
1 × Switzerland
2 × France
3 × United Kingdom
7 × USA
Collaborated with:T.W.Reps S.Qadeer M.Emmi N.Kidd S.K.Lahiri A.V.Nori J.Lim S.K.Rajamani G.Balakrishnan T.Touili S.Bindal S.Bansal S.Joshi Z.Pavlinovic R.Sharma P.Liu T.Wahl P.Deligiannis A.V.Thakur A.Das Y.Li A.T.Chaganty M.F.Atig A.Bouajjani W.R.Harris M.Polishchuk B.Liblit A.F.Donaldson J.Ketema P.Thomson V.Tulsian A.Kanade R.Kumar A.Haran M.Carter Z.Rakamaric R.S.0001 M.Costa N.P.Lopes S.A.Seshia K.Vaswani A.Burton E.Driscoll M.Elder T.Andersen Suvam Mukherjee Nitin John Raj Krishnan Govindraj Chandramouleswaran Ravichandran A.Rastogi Raja Krishnaswamy D.Melski R.Gruian S.H.Yong C.Chen T.Teitelbaum
Talks about:program (10) asynchron (4) analysi (4) verifi (4) machin (4) verif (4) use (4) termin (3) modulo (3) model (3)
Person: Akash Lal
DBLP: Lal:Akash
Facilitated 3 volumes:
Ed
ExpertReviewPaPrBoardContributed to:
2015
2015
2015
2014
20142013
201320122012
2012
20122010201020082008200820072006
2006200520162019
20192016Wrote 29 papers:
- CAV-2015-DasLLL #precise #verification
- Angelic Verification: Precise Verification Modulo Unknowns (AD, SKL, AL, YL), pp. 324–342.
- PLDI-2015-DeligiannisDKLT #analysis #programming #state machine #testing
- Asynchronous programming, analysis and testing with state machines (PD, AFD, JK, AL, PT), pp. 154–164.
- PLDI-2015-LalQ #graph #source code
- DAG inlining: a decision procedure for reachability-modulo-theories in hierarchical programs (AL, SQ), pp. 280–290.
- TACAS-2015-HaranCELQR #composition #contest #verification
- SMACK+Corral: A Modular Verifier — (Competition Contribution) (AH, MC, ME, AL, SQ, ZR), pp. 451–454.
- FSE-2014-LalQ #using #verification
- Powering the static driver verifier using corral (AL, SQ), pp. 202–212.
- MSR-2014-TulsianKKLN #algorithm #model checking #named
- MUX: algorithm selection for software model checkers (VT, AK, RK, AL, AVN), pp. 132–141.
- CAV-2013-ChagantyLNR #learning #relational #smt #using
- Combining Relational Learning with SMT Solvers Using CEGAR (ATC, AL, AVN, SKR), pp. 447–462.
- ISSTA-2013-BindalBL #bound #concurrent #parallel #source code #testing #thread
- Variable and thread bounding for systematic testing of multithreaded programs (SB, SB, AL), pp. 145–155.
- CAV-2012-AtigBEL #detection #parallel #source code #thread
- Detecting Fair Non-termination in Multithreaded Programs (MFA, AB, ME, AL), pp. 210–226.
- CAV-2012-LalQL #modulo theories #reachability
- A Solver for Reachability Modulo Theories (AL, SQ, SKL), pp. 427–443.
- FSE-2012-EmmiLQ #source code
- Asynchronous programs with prioritized task-buffers (ME, AL, SQ), p. 48.
- POPL-2012-JoshiLL #debugging
- Underspecified harnesses and interleaved bugs (SJ, SKL, AL), pp. 19–30.
- SAS-2012-EmmiL #distributed #source code
- Finding Non-terminating Executions in Distributed Asynchronous Programs (ME, AL), pp. 439–455.
- CAV-2010-RepsLTBL #verification
- There’s Plenty of Room at the Bottom: Analyzing and Verifying Machine Code (TWR, JL, AVT, GB, AL), pp. 41–56.
- CAV-2010-ThakurLLBDEAR #generative #proving
- Directed Proof Generation for Machine Code (AVT, JL, AL, AB, ED, ME, TA, TWR), pp. 288–305.
- SAS-2010-HarrisLNR #termination
- Alternation for Termination (WRH, AL, AVN, SKR), pp. 304–319.
- CAV-2008-LalR #analysis #bound #concurrent
- Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis (AL, TWR), pp. 37–51.
- SAS-2008-KiddLR #reduction
- Language Strength Reduction (NK, AL, TWR), pp. 283–298.
- SAS-2008-LalR #data flow #multi #query #using
- Solving Multiple Dataflow Queries Using WPDSs (AL, TWR), pp. 93–109.
- TACAS-2008-LalTKR #analysis #bound #concurrent #interprocedural #source code
- Interprocedural Analysis of Concurrent Programs Under a Context Bound (AL, TT, NK, TWR), pp. 282–298.
- SAS-2007-LalKRT #fault
- Abstract Error Projection (AL, NK, TWR, TT), pp. 200–217.
- CAV-2006-LalR #automaton #model checking
- Improving Pushdown System Model Checking (AL, TWR), pp. 343–357.
- ESOP-2006-LalLPL #debugging #optimisation #source code
- Path Optimization in Programs and Its Application to Debugging (AL, JL, MP, BL), pp. 246–263.
- CAV-2005-BalakrishnanRKLLMGYCT #bytecode #model checking
- Model Checking x86 Executables with CodeSurfer/x86 and WPDS++ (GB, TWR, NK, AL, JL, DM, RG, SHY, CHC, TT), pp. 158–163.
- CAV-2005-LalRB #automaton
- Extended Weighted Pushdown Systems (AL, TWR, GB), pp. 434–448.
- ASE-2016-PavlinovicLS #verification
- Inferring annotations for device drivers from verification histories (ZP, AL, RS), pp. 450–460.
- CAV-2019-LiuWL #source code #using #verification
- Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers (PL, TW, AL), pp. 386–404.
- ECOOP-2019-MukherjeeRGDRLR #framework #programming #reliability #state machine
- Reliable State Machines: A Framework for Programming Reliable Cloud Services (SM, NJR, KG, PD, CR, AL, AR, RK), p. 29.
- PLDI-2016-0001CLLRSV #design #verification
- A design and verification methodology for secure isolated regions (RS0, MC, AL, NPL, SKR, SAS, KV), pp. 665–681.