Akash Lal

Papers
Talks
Other Publications and Technical Reports
Software


Papers (CiteseerX, Google Scholar, Microsoft Libra, DB&LP )

Model Checking

• Symbolic Analysis via Semantic Reinterpretation. Junghee Lim, Akash Lal and Thomas Reps. In Proc. SPIN Workshop, 2009. [abstract; PDF; (c) Springer-Verlag]
• Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis. Akash Lal and Thomas Reps. In Formal Methods in System Design (FMSD) 35, 1 (2009). [abstract; PDF; (c) Springer-Verlag]
• Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis. Akash Lal and Thomas Reps. In Proc. Computer Aided Verification (CAV), 2008. (Invited for special submission to the Int. Journal on Formal Methods in System Design.) [abstract; PDF; (c) Springer-Verlag]
• Solving Multiple Dataflow Queries Using WPDSs. Akash Lal and Thomas Reps. In Proc. Static Analysis Symposium (SAS), 2008. [abstract; PDF; (c) Springer-Verlag]
• Language Strength Reduction. Nicholas Kidd, Akash Lal, and Thomas Reps. In Proc. Static Analysis Symposium (SAS), 2008. [abstract; PDF; (c) Springer-Verlag]
• Interprocedural Analysis of Concurrent Programs Under a Context Bound. Akash Lal, Tayssir Touili, Nicholas Kidd, and Thomas Reps. In Proc. 14th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008. [abstract; PDF; (c) Springer-Verlag]
• Program Analysis Using Weighted Pushdown Systems (Invited paper). Thomas Reps, Akash Lal, and Nicholas Kidd. In Proc. 27th Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 2007. [abstract; PDF; (c) Springer-Verlag]
• Abstract Error Projection. Akash Lal, Nicholas Kidd, Thomas Reps, and Tayssir Touili. In Proc. Static Analysis Symposium (SAS), 2007. [abstract; PDF; (c) Springer-Verlag]
• Improving Pushdown System Model Checking. Akash Lal and Thomas Reps. In Proc. Computer Aided Verification (CAV), 2006. [abstract; PDF; (c) Springer-Verlag]
• Path Optimization in Programs and its Application to Debugging. Akash Lal, Junghee Lim, Marina Polishchuk and Ben Liblit. In Proc. European Symposium on Programming (ESOP), 2006. (Nominated for the best paper award.) [abstract; PDF; (c) Springer-Verlag; Slides]
• Extended Weighted Pushdown Systems. Akash Lal, Gogul Balakrishnan and Thomas Reps. In Proc. Computer Aided Verification (CAV), 2005. [abstract; PDF; (c) Springer-Verlag; Slides]
• Modelchecking x86 executables with CodeSurfer/x86 and WPDS++ (tool-demonstration paper). Balakrishnan, G., Reps, T., Kidd, N., Lal, A., Lim, J., Melski, D., Gruian, R., Yong, S., Chen, C.-H., and Teitelbaum, T. In Proc. Computer Aided Verification (CAV), 2005. abstract; PDF; (c) Springer-Verlag]

• A Constraint Programming Approach to Cutset Problems. François Fages and Akash Lal. Computers and Operations Research Journal 33, 10 (Oct. 2006), 2852-2865. [abstract; PDF]

• A Global Constraint for Cutset Problems. François Fages and Akash Lal. Fifth International Workshop on Integration of AI and OR techniques in constraint programming for combinatorial optimization problems CPAIOR'03, Montreal, Canada. April 2003. [abstract; PostScript; PDF]

• Effective Chemistry for Synchrony and Asynchrony. Deepak Garg, Akash Lal and Sanjiva Prasad. IFIP WCC-TCS 2004, August 2004 , Toulouse, France. [abstract; PostScript; PDF]

• Reducing concurrent analysis under a context bound to sequential analysis,
  • Conference on Computer Aided Verification (CAV), Princeton, NJ, USA, July 2008.
  • LIAFA, Universite Paris Diderot - Paris 7, France, June 2008.
• Solving multiple dataflow queries using WPDSs,
  • Static Analysis Symposium (SAS), Valencia, Spain, July 2008.
  • LIAFA, Universite Paris Diderot - Paris 7, France, June 2008.
• Interprocedural analysis of concurrent programs under a context bound,
  • Ecole Normale Superieure (ENS), Paris, France, June 2008.
  • Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Budapest, Hungary, April 2008.
  • Microsoft Research, Bangalore, India, October 2007.
• Abstract error projection,
  • Static Analysis Symposium (SAS), Kongens Lyngby, Denmark, August 2007.
  • IBM Research, Hawthorne, USA, August 2007.
  • Microsoft Research, Bangalore, India, January 2007.
• PC-based abstractions,
  • Microsoft Research, Redmond, Washington, August 2006.
• Improving pushdown system model checking,
  • Conference on Computer Aided Verification (CAV), Seattle, WA, USA, July 2006.
• Path optimization in programs and its application to debugging,
  • European Symposium on Programming (ESOP), Vienna, Austria, April 2006.
• Extended weighted pushdown systems,
  • Microsoft Research, Redmond, Washington, July 2005.
  • IBM, India Research Lab, January 2006.
  • IIT-Delhi, New Delhi, India, January 2006.
  • Conference on Computer Aided Verification (CAV), Edinburgh, Scotland, July 2005.
• Affine relation analysis in x86 code,
  • ONR MURI review meeting, Arlington, Virginia, February 2005.

• Reference Count Analysis with Shallow Aliasing. Akash Lal, G. Ramalingam. Tech. Report MSR-TR-2009-61, Microsoft Research. May 2009. [paper]

• McDASH: Refinement-based property verification for machine code. Akash Lal, Junghee Lim and Thomas Reps. Tech. Report TR-1659, Computer Sciences Department, University of Wisconsin, Madison. January 2008. [abstract; PDF]

• Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis. Akash Lal and Thomas Reps. Tech. Report TR-1629, Computer Sciences Department, University of Wisconsin, Madison. January 2008. [PDF]

• Interprocedural Analysis of Concurrent Programs under a Context Bound. Akash Lal, Tayssir Touili, Nicholas Kidd, and Thomas Reps. Tech. Report TR-1598, Computer Sciences Department, University of Wisconsin, Madison. July 2007. [abstract; PDF]

• Weighted Pushdown Systems and Weighted Transducers. Akash Lal, Tayssir Touili, Nicholas Kidd, and Thomas Reps. Tech. Report TR-1581, Computer Sciences Department, University of Wisconsin, Madison. October 2006. [abstract; PDF]

• Abstract Error Projection. Akash Lal, Nicholas Kidd, Thomas Reps, and Tayssir Touili. Tech. Report TR-1579, Computer Sciences Department, University of Wisconsin, Madison. September 2006. [abstract; PDF]

• Improving Pushdown System Model Checking. Akash Lal and Thomas Reps. Tech. Report TR-1552, Computer Sciences Department, University of Wisconsin, Madison. January 2006. [abstract; PDF]

• BTrace: Path Optimization for Debugging. Akash Lal, Junghee Lim, Marina Polishchuk, Ben Liblit. Tech. Report TR-1535, Computer Sciences Department, University of Wisconsin, Madison. October 2005. [abstract; PDF]
  

• Model checking x86 executables with CodeSurfer/x86 and WPDS++. Balakrishnan, G., Reps, T., Kidd, N., Lal, A., Lim, J., Melski, D., Gruian, R., Yong, S., Chen, C.-H., and Teitelbaum, T.,  In Proc. Workshop on the Evaluation of Software Defect Detection Tools, June 2005. [Co-located with PLDI05.]

• Graph Isomorphism for Colored Graphs with Color Multiplicity Bounded by 3. Akash Lal and Dieter van Melkebeek. Tech. Report TR-1523, Computer Sciences Department, University of Wisconsin, Madison. February 2005. [abstract; PostScript; PDF]

• WALi : The Weighted Automaton Library.
• WPDS++ : A C++ implementation of weighted pushdown systems.