NEW I have graduated from CMU
and will be joining Microsoft
Research, Redmond towards the end of September '04.
I am a 5th year doctoral student in Computer Engineering in the Electrical and Computer Eng. Dept, at CMU. I work with Prof. Randy Bryant in formal verification. I completed my undergraduate from Indian Institute of Technology, Kharagpur, India in June'99 at the Department of Computer Science and Engg .
I finished my Masters in Electrical and Computer Engineering (ECE) Dept, at CMU in May 2001. Currently I am a PhD candidate in ECE, CMU.
Spring '00
Fall ' 99"Experience
with Term-level Modeling and Verification of the M*CORE
microprocessor Core",
Shuvendu K. Lahiri, Carl Pixley,
Ken Albin.
In Proc. IEEE Workshop on High Level Design
Validation and Test (HLDVT) Workshop, Monterey, USA,
Nov 2001.
"Modeling and
Verifying Systems using a Logic of Counter Arithmetic with Lambda
Expressions and Uninterpreted Functions"
Randal E. Bryant, Shuvendu K. Lahiri,
and Sanjit A. Seshia.
In Proc. Computer-Aided Verification
(CAV '02), LNCS 2404, Springer-Verlag, Pages 78 - 92, Copenhagen, Denmark, July
2002
"Modeling and
Verification of Out-of-order Microprocessors in UCLID"
Shuvendu K. Lahiri, Sanjit A. Seshia,
and Randal E. Bryant.
In Proc. International Conference on
Formal Methods in Computer-Aided Design (FMCAD '02),
LNCS 2517, Springer-Verlag, Pages 142 - 158, Portland,
USA, November 2002.
"Deciding
CLU Logic Formulas via Boolean and Pseudo-Boolean Encodings"
Randal E. Bryant, Shuvendu K. Lahiri,
and Sanjit A. Seshia.
In Proc. Intl. Workshop on Constraints
in Formal Verification , September 2002. Associated with
Intl. Conf. on Principles and Practice of Constraint Programming.
"A Hybrid
SAT-based Decision Procedure for Separation Logic with Uninterpreted
Functions"
Sanjit A. Seshia, Shuvendu K. Lahiri,
Randal E. Bryant.
In Proc. Design Automation Conference
(DAC '03), ACM Press, Pages: 425 - 430, Anaheim, CA, USA, June 2003.
"Deductive Verification
of Advanced Out-of-Order Microprocessors"
Shuvendu K. Lahiri and Randal E.
Bryant.
In Proc. of Computer-Aided Verification
(CAV 03), LNCS 2725, Springer-Verlag, Pages 341-354, Colorado, USA, July 2003
"A Symbolic
Approach to Predicate Abstraction"
Shuvendu K. Lahiri, Randal
E. Bryant and Byron Cook.
In Proc. of Computer-Aided Verification
(CAV 03), LNCS 2725,
Springer-Verlag, Pages 141-153, Colorado, USA,
July 2003
"Convergence
Testing in Term-level Bounded Model Checking"
Randal E. Bryant, Shuvendu K. Lahiri and Sanjit A.
Seshia.
In Proc. of 12th Conference on Correct
Hardware Design and Verification Methods (CHARME), LNCS 2860, Springer-Verlag, Pages 348-362, L'Aquila, Italy, October
2003.
"Constructing
Quantified Invariants via Predicate Abstraction"
Shuvendu K. Lahiri and Randal E. Bryant
In Proc. of 5th Intl. Conference on Verification,
Model Checking and Abstract Interpretation (VMCAI), LNCS 2937, Springer-Verlag, Pages 267-281, Venice, Italy, January 2004.
"Revisiting
Positive Equality"
Shuvendu K. Lahiri, Randal E. Bryant, Amit Goel and Muralidhar
Talupur
In Proc. of 10th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems (TACAS), Barcelona, March
2004 (to appear)
"Indexed
Predicate Discovery for Unbounded System Verification"
Shuvendu K. Lahiri, Randal E. Bryant
In Proc. of Computer-Aided Verification
(CAV 04), Boston, July 2004 (to appear)
"The
UCLID Decision Procedure"
Shuvendu K. Lahiri, Sanjit A. Seshia
(Tool Description) In Proc. of Computer-Aided
Verification (CAV 04), Boston, July 2004 (to appear)
"Zapato:
Automatic theorem proving for predicate abstraction refinement"
Thomas Ball, Byron Cook, Shuvendu K. Lahiri and Lintao Zhang
(Tool Description) In Proc. of Computer-Aided
Verification (CAV 04), Boston, July 2004 (to appear)
"An efficient
decision procedure for the logic of Counters, Constrained Lambda
expressions, Uninterpreted Functions and Ordering"
Shuvendu K. Lahiri.
Masters Thesis, ECE Department, CMU, May
2001.
"Comparing
Techniques for Out-of-Order Processor Verification in UCLID"
Shuvendu K. Lahiri, Sanjit A. Seshia
and Randal E. Bryant
Proc. of SRC TECHCON, Dallas, USA,
August 2003.
"Convergence
Testing in Term-level Bounded Model Checking"
Randal E. Bryant, Shuvendu K. Lahiri and Sanjit.
A. Seshia
Computer Science Department Technical report CMU-CS-03-156,
2003.
"Revisiting
Positive Equality"
Shuvendu K. Lahiri, Randal E. Bryant, Amit Goel and
Muralidhar Talupur
Computer Science Department Technical report CMU-CS-03-196,
2003.
Presentations (coming soon)
02/01/00