Deprecated : The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Ashish Tiwari's Homepage
Ashish Tiwari
Research Interests
Decision Procedures: Equational Reasoning, Term Rewriting;
Current Professional Activities
Program Committees: Please consider submitting to the following conferences:
Algebraic Biology 2007 , July 2-4, 2007, Hagenberg, Austria. (Submission deadline: Dec 4th/11th)
CSL 2007 , Lausanne, Sept 11-15, 2007.
CAV 2007 , Berlin, July 3-7, 2007.
SMT 2007 , Berlin, July 1-2, 2007.
Past PC Participation .
Publicity: Please consider submitting and attending
RTA 2007 / RDP 2007 .
Ongoing Projects
New Research Articles
Disseration/Conference Tutorials/Talks
Combining abstract interpreters,
Stanford talk (in ps) and
Stanford talk (in pdf) .
With Harald Ruess and N. Shankar,
On Shostak's Combination
of Decision Procedures . Tutorial at CADE 2002, Copenhagen. Click on the above link for slides.
Decision procedures in automated deduction, Dissertation
in postscript ,
gzipped postscript , and
pdf , Department of Computer Science,
State University of New York at Stony Brook, 2000. Advisor
Prof. Leo Bachmair .
Decision procedures summer school:
Aug 9-11, Stanford .
Research Publications (reverse chronological order)
With Sumit Gulwani,
Computing Procedure Summaries for Interprocedural Analysis" (in ps).
To appear in ESOP 2007.
With Sumit Gulwani,
"Assertion checking unified" (in ps).
To appear in VMCAI 2007.
Preliminary version also available as MSR-TR-2006-99.
With Alessandro Abate,
"Box invariance of Hybrid and Switched Systems" ,
2nd IFAC Conference on Analysis and Design of Hybrid Systems, ADHS 2006 .
To appear.
Full paper .
With S. Gulwani,
"Combining abstract interpreters" .
PLDI 2006. This paper introduces the logical product of two logical
lattices. It then shows that abstract interpreters over the individual
logical lattices can be combined to yield the most precise abstract
interpreter over the logical product under certain conditions on
the logical theories defining the logical lattices. The combination
result (and the conditions) are inspired by the Nelson-Oppen combination
result for deciding satisfiability in the disjoint union of
stably-infinite theories.
With S. Gulwani,
"Assertion Checking in the Combined Abstraction of Linear Arithmetic and Uninterpreted Functions" . ESOP 2006. This paper shows that assertion checking
over the combination of two logical lattices can be hard, even when it is
PTime over the individual lattices.
With Linda Briesemeister and Phil A. Porras,
"Model checking of worm quarantine and counter-quarantine under a
group defense" , SRI Technical Report, Oct 2005.
With G. Godoy,
"Confluence of shallow right-linear rewrite systems" .
In
CSL 2005 .
We show that the following problem is surprisingly decidable:
given a shallow and right-linear rewrite system, determine if it is confluent.
(Preliminary version, to be revised)
A. Tiwari,
"An algebraic approach to the satisfiability of nonlinear constraints" .
In
CSL 2005 .
This paper presents a pragmatic and powerful
sound and refutationally complete method for testing satisfiability
of nonlinear constraints over the reals.
(Preliminary version, to be revised)
With Guillem Godoy,
Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules
. In CADE 2005.
(Preliminary version, to be revised)
With E. Rodriguez-Carbonell,
"Generating Polynomial Invariants for Hybrid Systems",
In Hybrid Systems: Computation and Control 2005.
With S. Gulwani and G. Necula,
"Join Algorithms for the theory of uninterpreted functions",
In K. Lodaya and M. Mahajan (eds.)
FSTTCS 2004, Vol 3328 of LNCS, p.311-323, 2004.
A. Tiwari,
"Termination of linear programs" . In CAV 2004.
This paper shows decidability of termination for a class of linear loop programs.
With Guillem Godoy,
"Deciding fundamental properties of right-ground or right-variable systems by rewrite closure" .
In IJCAR 2004.
This paper shows decidability of properties such as reachability, joinability,
confluence, and termination for TRSs containing right-ground or collapsing rules.
With Leonardo de Moura, Sam Owre, Harald Ruess, John Rushby, N. Shankar, and Maria Sorea,
SAL 2 . In CAV 2004.
With Guillem Godoy and Rakesh Verma,
"Confluence characterization using rewrite closure with
application to right ground systems" .
This paper presents a solution of
open problem #63
from the
RTA list of open problems .
In
AAECC .
With P. Lincoln,
"
"Symbolic systems biology: Hybrid modeling and analysis of biological networks" ,
In HSCC 2004.
With N. Berregeb and R. Robbana,
"Toward Automatic Proofs of Observational Properties" ,
Discrete Mathematics and Theoretical Computer Science 6(2), 143--162, 2004.
With G. Khanna,
"
Nonlinear Systems: Approximating Reach Sets ",
In HSCC 2004.
With Guillem Godoy and Rakesh Verma,
"Deciding confluence of certain term rewriting systems in polynomial time",
Annals of Pure and Applied Logic , APAL 130(1-3):33-59, December 2004.
Ashish Tiwari,
"Abstraction based theorem proving: An example from the theory of reals ",
In the proceedings of the
PDPAR 2003
workshop, colocated with
CADE 2003 .
Ashish Tiwari,
"Approximate Reachability for Linear Systems ",
In the Proceedings of Hybrid Systems: Computation and Control,
HSCC 2003 .
With Ronojoy Ghosh and
Claire Tomlin ,
"Automated Symbolic
Reachability Analysis with Application to Delta-Notch Signaling Automata ",
In the Proceedings of Hybrid Systems: Computation and Control,
HSCC 2003 .
With Guillem Godoy and
Rakesh Verma ,
"On the confluence of linear shallow term rewrite systems ",
In
STACS 2003 , 20th International Symposium on Theoretical Aspects of Computer Science,
Feb 27--Mar 01, 2003.
With N. Shankar and J. Rushby,
"Invisible formal
methods for embedded control systems ",
In Proc of the IEEE, Special issue on Embedded Systems, Jan 2003.
With Guillem Godoy and
Robert Nieuwenhuis ,
"Classes of Term Rewrite Systems
with Polynomial Confluence Problems ",
(journal article) To appear in TOCL ,
Volume 5, Number 2 (April 2004).
Ashish Tiwari,
"Polynomial Time Algorithms for Deciding Confluence of Certain Term Rewrite Systems" ,
In IEEE Symposium on Logic in Computer Science, LICS 2002.
Context .
With G. Khanna ,
"Series of Abstractions for Hybrid Automata" ,
In Hybrid Systems: Computation and Control, HSCC 2002.
With Leo Bachmair and Laurent Vigneron,
"Abstract Congruence Closure" ,
J. of Automated Reasoning 31(2), 2003, pp. 129--168, Kluwer Academic Publishers.
Ashish Tiwari,
"Rewrite Closures for Ground and Cancellative AC Theories" ,
In FST&TCS; 2001, LNCS 2245.
With Harald Ruess, Hassen Saidi and N. Shankar,
"Automatic Generation of Invariants" ,
In
TACAS 2001 - Tools and Algorithms for the Construction and Analysis of Systems.
S. Bensalem, et. al.,
"An overview of SAL",
In
Langley Workshop on Formal Methods,
LFMW 2000 .
With Leo Bachmair,
"Abstract Congruence Closure and Specializations" ,
17th Intl Conference on Automated Deduction,
CADE 2000 .
With Leo Bachmair and Harald Ruess,
"Rigid E-Unification Revisited" ,
17th Intl Conference on Automated Deduction,
CADE 2000 .
With R. K. Ahuja and James B. Orlin,
"A Greedy Genetic Algorithm for the Quadratic Assignment Problem",
Working paper, Sloan
School of Management, WP\#3826-95, June 1995. Also in
Computers and Operations Research 27 (10), Sept. 2000, pp. 917--934.
With Leo Bachmair, I.V. Ramakrishnan, and L. Vigneron,
"Congruence Closure modulo Associativity and Commutativity",
Workshop on Frontiers of Combining Systems,
FroCos 2000 ,
LNAI 1794.
With Leo Bachmair, C. Ramakrishnan and I.V. Ramakrishnan,
"Normalization via Rewrite Closures" ,
Rewriting Techniques and
Applications, Proceedings of the
10th RTA-1999 .
With Leo Bachmair,
"D-bases for Polynomial Ideals over Commutative Noetherian Rings" ,
Rewriting Techniques and
Applications,
Proceedings of the
8th RTA-1997 , pp. 113-127.
Software
Other Papers
Talks
Hybrid modeling and analysis of biological networks .
Talk at the Workshop on
Logic in Systems Biology, LSB, co-located with FLoC 2006,
Aug 15, 2006.
Hybrid modeling and analysis of genetic networks. Talk at
Univ of Notre Dame, Feb 27, 2004.
"Symbolic techniques for verification of hybrid systems" (ps) ,
Talk at CMU, Sep 30, 2003.
(HybridAbstraction + Composition + Systems Biology)
"Symbolic methods for verification of hybrid systems" (ps) ,
Presentation at the NASA Ames Research Center, Mountain View, CA, June 17, 2003.
Talks with the only slightly different content were also given at
Dagstuhl Seminar on Theorem Proving and Infinite State Model-Checking (April 21--25, 2003),
and MPI Saarbrucken (April 30--May 2, 2003).
"Symbolic methods for verification of hybrid systems" (ps) ,
Presentation at the Hybrid Systems Seminar series, University of
Pennsylvania, Philadelphia, Feb 28, 2003.
"Combining Decision Procedures" (pdf) ,
Presentation at the Stanford Logic Seminar, Oct 15, 2002.
Also available in
in postscript .
"SRI/UT Proposal Slides for NEST" (pdf) ,
Also available in
4up format (pdf) .
Al Mok,
"SRI/UT Demo Plan for NEST" (ppt) ,
Presentation for the NEST OEP Meeting at St. Louis, Aug 23rd.
See
here
and
here
for postscript.
With Pat Lincoln and John Rushby,
"Formal Composition for Time-Triggered Systems" ,
Presentation for the MoBIES PI meeting at New York on July 25th.
A. Tiwari,
"Stanford Talk" .
A. Tiwari,
"Uniform description of efficient decision procedures using extended signatures" ,
MacLean Hall, Computer Science Department, University of Iowa, Iowa City, Mar 1, 2002.
In pdf
A. Tiwari,
"Formal Methods for Analysis of Hybrid Systems" ,
Room 339, Cory Hall, UC Berkeley, Feb 11, 2002.
A. Tiwari,
"Formal Methods for Analysis of Hybrid Systems" ,
Durand 026, Stanford University, Dec 07, 2001.
A. Tiwari,
"Formal Composition for Time-Triggered Systems" ,
Presented at MoBIES ESWG meeting at Dearbon.
Ashish Tiwari,
"Abstract Congruence Closure and Applications",
Dagstuhl seminar on Deduction, Seminar No. 99091,
Report No. 232, U. Furbach (Koblenz), H. Ganzinger
(MPI-Saarbrücken), D. Kapur (Albany), 28 Feb--5 March 1999.
Ashish Tiwari,
"Grobner bases for polynomial ideals over commutative Noetherian rings",
Talk given at Chennai Mathematical Institute, Jan. 1999.
Ashish Tiwari,
"Decision Procedures in Automated Deduction",
Preliminary Examination Report,
PhD Proposal, SUNY at Stony Brook, Nov 1998.
Miscellaneous Areas: Reports
Ashish Tiwari,
"Adding BDD's to the Concurrency Factory's Local Model Checker",
CSE 635 Asynchronous Systems, Project Report, Spring 1997.
Zhong Li and Ashish Tiwari,
"Addition Chain Heuristics/RSA Public Key Cryptosystem",
CSE 502 Computer Architecture, Project Report, Spring 1996.
Ashish Tiwari,
"Identifying Mathematical and Logical Sequences",
CSE 539 Expert Systems, Project Report, Spring 1996.
Ashish Tiwari,
"Group Testing", (.ps.Z)
CSE 648 Advanced Algorithms, Project Report, Fall 1995.
Ashish Tiwari,
"Sweeping a 3-D Tetrahedral Complex",
CSE 528 Computer Graphics, Project Report, Fall 1995. Appeared as part of
"Fast Rendering of Irregular Grids", by Claudio T.Silva,
J.S.B. Mitchell and Arie E. Kaufman, ACM/IEEE Volume
Visualization Symposium 1996, pp. 15--22.
Teaching
Fall 2003: CS359: Little Engines of Proof , Stanford University.
Automata Theory, Summer (1997) term special couse for incoming graduate students, SUNY-Stony Brook.
Teaching Assistant for CSE 113
"Foundations of Computer Science I", Fall 1995,
Instructor:
Prof. P.B.Henderson.
Teaching Assistant for CSE 213,
"Foundations of Computer Science II", Spring 1996,
Instructor:
Prof. Leo Bachmair .
Teaching Assistant for CSE 506,
"Operating Systems",
Spring 1996,
Instructor:
Prof. Gene Stark .
Miscellaneous: Useful Links/Upcoming Conferences
SRI Insider IEEE info .
Personal Page , for photographs.
Past PC participation:
HSCC 2006: Hybrid Systems: Computation and Control , Mar 29--31, Santa Barbara (Program Chair).
RTA 2006: Rewriting Techniques and Applications , Aug 12-15, 2006, Seattle, Wasington
PDPAR 2006: Pragmatics of Decision Procedures in Automated Reasoning , Aug 21, 2006, Seattle, Wasington
FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science , Dec 13-15, 2006, Indian Statistical Institute (ISI), Kolkata
LPAR-12, 2005: 12th Intl. Conf. on Logic for Programming Artificial Intelligence and Reasoning , Montego Bay, Jamaica, 2nd-6th Dec 2005.
FroCoS 2005: Frontiers of Combining Systems , Sept 19-21, 2005, Vienna.
CADE-20, 2005: Conf. on Automated Deduction .
HSCC-2005: Hybrid Systems: Computation and Control , Mar 9--11, Zurich.
IJCAR 2004: Intl Joint Conf on Automated Reasoning .
RTA 2004: Intl Conf on Rewriting Techniques and Applications .
HSCC 2003: Hybrid Systems: Computation and Control .
RTA 2003: Rewriting Techniques and Applications RTA 2003 .
See also RDP03-RTA page .
PDPAR 2003: Pragmatics of Decision Procedures in Automated Reasoning 2003 .
Stefan Ratschan,
Applications of the decision procedure for reals .
NSF,
CISE page . Goto funding oppurtunities/program of interest there.
NIH,
NIH guide for grants and contracts,
with links to PAs and RFAs .
Darpa solicitations
Click here .
LICS,
IEEE Symposium on Logic in Computer Science . Deadline Jan 6th/13th.
The
LICS newsletter .
CADE,
CADE-19 . Deadline Jan 24th/Jan 31st.
CSL Generic Page
and CSL 2003 specific page . Deadline: 31st March
LPAR,
LPAR . Deadline Apr 28/May 5th.
FSTTCS Generic page . Deadline: July 1.
BioInformatics Conference,
IEEE Computer Society, BioInformatics Conference . Deadline Apr 01, 2003.
HSIF,
HSIF .
DBLP,
my link .
Counseling:
Here or
here! .
Off : EL 270, SRI Intl., 333 Ravenswood Ave, Menlo Park, CA 94025. Tel : 650-859-4774 Personal
home page
Ashish Tiwari (Email: tiwari _AT_ csl _DOT_ sri _DOT_ com)
Back to department home page