| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Natarajan Shankar, K. Subramani |
A mechanical verification of the stressing algorithm for negative cost cycle detection in networks.  |
Sci. Comput. Program.  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Pritam Roy, Natarajan Shankar |
SimCheck: a contract type system for Simulink. |
ISSE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar, Marc Vaucher |
The Mechanical Verification of a DPLL-Based Satisfiability Solver. |
Electr. Notes Theor. Comput. Sci. |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Vladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark A. Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, Benjamin Weiß |
The 1st Verified Software Competition: Experience Report. |
FM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Sam Owre, Natarajan Shankar |
Solving the First Verified Software Competition Problems Using PVS. |
Formal Modeling: Actors, Open Systems, Biological Systems |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Tony Hoare, Natarajan Shankar |
Unraveling a Card Trick. |
Essays in Memory of Amir Pnueli |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar |
Rewriting, Inference, and Proof. |
WRLA |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | C. A. R. Hoare, Jayadev Misra, Gary T. Leavens, Natarajan Shankar |
The verified software initiative: A manifesto. |
ACM Comput. Surv. |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar |
Automated deduction for verification. |
ACM Comput. Surv. |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Ashish Gehani, Florent Kirchner, Natarajan Shankar |
System Support for Forensic Inference. |
IFIP Int. Conf. Digital Forensics |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar |
Trust and Automation in Verification Tools. |
ATVA |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar |
Fixpoints and Search in PVS. |
LASER Summer School |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar, Jim Woodcock (eds.) |
Verified Software: Theories, Tools, Experiments, Second International Conference, VSTTE 2008, Toronto, Canada, October 6-9, 2008. Proceedings |
VSTTE |
2008 |
DBLP BibTeX RDF |
|
| 1 | Sam Owre, Natarajan Shankar |
A Brief Overview of PVS. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Leonardo Mendonça de Moura, Bruno Dutertre, Natarajan Shankar |
A Tutorial on Satisfiability Modulo Theories. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Ulrich Furbach, Natarajan Shankar (eds.) |
Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings |
IJCAR |
2006 |
DBLP BibTeX RDF |
|
| 1 | Leonardo Mendonça de Moura, Harald Rueß, Natarajan Shankar |
Justifying Equality. |
Electr. Notes Theor. Comput. Sci. |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar |
Inference Systems for Logical Algorithms. |
FSTTCS |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar |
The ICS Decision Procedures for Embedded Deduction. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar, Maria Sorea, Ashish Tiwari |
SAL 2. |
CAV |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Ashish Tiwari, Natarajan Shankar, John M. Rushby |
Invisible formal methods for embedded control systems. |
Proceedings of the IEEE |
2003 |
DBLP BibTeX RDF |
|
| 1 | Jonathan Ford, Natarajan Shankar |
Formal Verification of a Combination Decision Procedure. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar, Harald Rueß |
Combining Shostak Theories. |
RTA |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar |
Little Engines of Proof. |
FME |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar |
Verification by Abstraction. |
10th Anniversary Colloquium of UNU/IIST |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar |
Little Engines of Proof. |
LICS |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Ashish Tiwari, Harald Rueß, Hassen Saïdi, Natarajan Shankar |
A Technique for Invariant Generation. |
TACAS |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar |
Using Decision Procedures with a Higher-Order Logic. |
TPHOLs |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Jean-Christophe Filliâtre, Sam Owre, Harald Rueß, Natarajan Shankar |
ICS: Integrated Canonizer and Solver. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Harald Rueß, Natarajan Shankar |
Deconstructing Shostak. |
LICS |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar |
Static Analysis for Safe Destructive Updates in a Functional Language. |
LOPSTR |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar |
Combining Theorem Proving and Model Checking through Symbolic Analysis. |
CONCUR |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar |
Symbolic Analysis of Transition Systems. |
Abstract State Machines |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Harald Rueß, Natarajan Shankar, Mandayam K. Srivas |
Modular Verification of SRT Division. |
Formal Methods in System Design |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar, Sam Owre |
Principles and Pragmatics of Subtyping in PVS. |
WADT |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Sandeep S. Kulkarni, John M. Rushby, Natarajan Shankar |
A case-study in component-based mechanical verification of fault-tolerant programs. |
WSS |
1999 |
DBLP BibTeX RDF |
|
| 1 | Hassen Saïdi, Natarajan Shankar |
Abstract and Model Check While You Prove. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby, Sam Owre, Natarajan Shankar |
Subtypes for Specifications: Predicate Subtyping in PVS. |
IEEE Trans. Software Eng. |
1998 |
DBLP DOI BibTeX RDF |
typechecking, Formal methods, consistency, type systems, specification languages, subtypes, PVS |
| 1 | Shaz Qadeer, Natarajan Shankar |
Verifying a self-stabilizing mutual exclusion algorithm. |
PROCOMET |
1998 |
DBLP BibTeX RDF |
|
| 1 | Sam Owre, John M. Rushby, Natarajan Shankar, David W. J. Stringer-Calvert |
PVS: An Experience Report. |
FM-Trends |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli, Natarajan Shankar, Eli Singerman |
Fair Synchronous Transition Systems and Their Liveness Proofs. |
FTRTFT |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Sam Owre, John M. Rushby, Natarajan Shankar |
Integration in PVS: Tables, Types, and Model Checking. |
TACAS |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar |
Lazy Compositional Verification. |
COMPOS |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | S. P. Rajan, Natarajan Shankar, Mandayam K. Srivas |
Industrial Strength Formal Verification Techniques for Hardware Designs. |
VLSI Design |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar |
Steps Toward Mechanizing Program Transformations Using PVS. |
Sci. Comput. Program. |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | David Cyrluk, Patrick Lincoln, Natarajan Shankar |
On Shostak's Decision Procedure for Combinations of Theories. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar |
PVS: Combining Specification, Proof Checking, and Model Checking. |
FMCAD |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Klaus Havelund, Natarajan Shankar |
Experiments in Theorem Proving and Model Checking for Protocol Verification. |
FME |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Sam Owre, S. Rajan, John M. Rushby, Natarajan Shankar, Mandayam K. Srivas |
PVS: Combining Specification, Proof Checking, and Model Checking. |
CAV |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Harald Rueß, Natarajan Shankar, Mandayam K. Srivas |
Modular Verification of SRT Division. |
CAV |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar |
Unifying Verification Paradigms. |
FTRTFT |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Sam Owre, John M. Rushby, Natarajan Shankar, Friedrich W. von Henke |
Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS. |
IEEE Trans. Software Eng. |
1995 |
DBLP DOI BibTeX RDF |
verification systems, fault tolerance, formal specification, formal methods, theorem proving, clock synchronization, PVS, Byzantine agreement, hardware verification, flight control |
| 1 | S. Rajan, Natarajan Shankar, Mandayam K. Srivas |
An Integration of Model Checking with Automated Proof Checking. |
CAV |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar |
Computer-Aided Computing. |
MPC |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Patrick Lincoln, Andre Scedrov, Natarajan Shankar |
Decision Problems for Second-Order Linear Logic |
LICS |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Sam Owre, John M. Rushby, Natarajan Shankar, Mandayam K. Srivas |
A Tutorial on Using PVS for Hardware Verification. |
TPCD |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | David Cyrluk, S. Rajan, Natarajan Shankar, Mandayam K. Srivas |
Effective Theorem Proving for Hardware Verification. |
TPCD |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Patrick Lincoln, Natarajan Shankar |
Proof Search in First-Order Linear Logic and Other Cut-Free Sequent Calculi |
LICS |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Jens Ulrik Skakkebæk, Natarajan Shankar |
Towards a Duration Calculus Proof Assistant in PVS. |
FTRTFT |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Patrick Lincoln, Andre Scedrov, Natarajan Shankar |
Linearizing Intuitionistic Implication. |
Ann. Pure Appl. Logic |
1993 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar |
David A. McAllester, Ontic: A Knowledge Representation System for Mathematics. |
Artif. Intell. |
1993 |
DBLP DOI BibTeX RDF |
|
| 1 | Sam Owre, John M. Rushby, Natarajan Shankar, Friedrich W. von Henke |
Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned. |
FME |
1993 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar |
Verification of Real-Time Systems Using PVS. |
CAV |
1993 |
DBLP DOI BibTeX RDF |
|
| 1 | Patrick Lincoln, John C. Mitchell, Andre Scedrov, Natarajan Shankar |
Decision Problems for Propositional Linear Logic. |
Ann. Pure Appl. Logic |
1992 |
DBLP DOI BibTeX RDF |
|
| 1 | Sam Owre, John M. Rushby, Natarajan Shankar |
PVS: A Prototype Verification System. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar |
Proof Search in the Intuitionistic Sequent Calculus. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar |
Mechanical Verification of a Generalized Protocol for Byzantine Fault Tolerant Clock Synchronization. |
FTRTFT |
1992 |
DBLP DOI BibTeX RDF |
|
| 1 | Patrick Lincoln, Andre Scedrov, Natarajan Shankar |
Linearizing Intuitionistic Implication |
LICS |
1991 |
DBLP DOI BibTeX RDF |
|
| 1 | Patrick Lincoln, John C. Mitchell, Andre Scedrov, Natarajan Shankar |
Decision Problems for Propositional Linear Logic |
FOCS |
1990 |
DBLP DOI BibTeX RDF |
noncommutative propositional linear logic, propositional linear logic, multiplicative fragment, unrestricted weakening, NP-completeness, undecidability, decision problem, PSPACE-complete |
| 1 | Natarajan Shankar, V. Ramachandran |
Efficient Parallel Circuits and Algorithms for Division. |
Inf. Process. Lett. |
1988 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar |
A mechanical proof of the Church-Rosser theorem. |
J. ACM |
1988 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar |
Towards Mechanical Metamathematics. |
J. Autom. Reasoning |
1985 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")