BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Belgium
1 × Greece
1 × Russia
1 × Spain
2 × Cyprus
2 × Germany
2 × Ireland
2 × The Netherlands
2 × United Kingdom
3 × France
3 × Italy
5 × Denmark
8 × USA
Collaborated with:
S.Owre H.Rueß J.M.Rushby P.Lincoln M.K.Srivas H.Saïdi L.M.d.Moura A.Scedrov S.Rajan J.Ford K.Havelund A.Tiwari G.Malecha A.Gehani C.Cheng I.Saha B.Dutertre D.Cyrluk M.P.Bonacina S.Graham-Lengrand S.Cruanes G.Hamon J.Filliâtre D.W.J.Stringer-Calvert F.W.v.Henke B.Zheng W.Li P.Deng L.Gérard Q.Zhu M.Sorea V.Klebanov P.Müller G.T.Leavens V.Wüstholz E.Alkassar R.Arthan D.Bronish R.Chapman E.Cohen M.A.Hillebrand B.Jacobs K.R.M.Leino R.Monahan F.Piessens N.Polikarpova T.Ridge J.Smans S.Tobies T.Tuerk M.Ulbrich B.Weiß
Talks about:
verif (7) proof (7) check (7) model (5) pvs (5) theori (4) system (4) integr (4) combin (4) decis (4)

Person: Natarajan Shankar

DBLP DBLP: Shankar:Natarajan

Facilitated 1 volumes:

IJCAR 2006Ed

Contributed to:

DAC 20152015
SAC 20152015
CADE 20132013
CAV 20132013
VMCAI 20132013
FM 20122012
SMT 20122012
FM 20112011
WRLA 20102010
CAV 20072007
CAV 20042004
IJCAR 20042004
CADE 20022002
FME 20022002
LICS 20022002
RTA 20022002
CAV 20012001
LICS 20012001
LOPSTR 20012001
TACAS 20012001
CAV 19991999
FM-Trends 19981998
TACAS 19971997
CADE 19961996
CAV 19961996
FME 19961996
CAV 19951995
LICS 19951995
LICS 19941994
CAV 19931993
FME 19931993
CADE 19921992
LICS 19911991
CADE 20172017

Wrote 36 papers:

DAC-2015-ZhengLDGZS #design #security #verification
Design and verification for transportation system security (BZ, WL, PD, LG, QZ, NS), p. 6.
SAC-2015-MalechaGS #automation
Automated software winnowing (GM, AG, NS), pp. 1504–1511.
CADE-2013-Shankar #automation #performance #reasoning
Automated Reasoning, Fast and Slow (NS), pp. 145–161.
CAV-2013-ChengRS #constraints #named #polynomial
JBernstein: A Validity Checker for Generalized Polynomial Constraints (CHC, HR, NS), pp. 656–661.
VMCAI-2013-CruanesHOS #integration #tool support
Tool Integration with the Evidential Tool Bus (SC, GH, SO, NS), pp. 275–294.
FM-2012-OwreSS #analysis #automation #cyber-physical
Automatic Dimensional Analysis of Cyber-Physical Systems (SO, IS, NS), pp. 356–371.
SMT-2012-Shankar #architecture #smt
The Architecture of Inference from SMT to ETB (NS), p. 2.
FM-2011-KlebanovMSLWAABCCHJLMPPRSTTUW #case study #contest #experience
The 1st Verified Software Competition: Experience Report (VK, PM, NS, GTL, VW, EA, RA, DB, RC, EC, MAH, BJ, KRML, RM, FP, NP, TR, JS, ST, TT, MU, BW), pp. 154–168.
WRLA-2010-Shankar #proving
Rewriting, Inference, and Proof (NS), pp. 1–14.
CAV-2007-MouraDS #modulo theories #satisfiability #tutorial
A Tutorial on Satisfiability Modulo Theories (LMdM, BD, NS), pp. 20–36.
SAL 2 (LMdM, SO, HR, JMR, NS, MS, AT), pp. 496–500.
IJCAR-2004-MouraORRS #deduction #embedded
The ICS Decision Procedures for Embedded Deduction (LMdM, SO, HR, JMR, NS), pp. 218–222.
CADE-2002-FordS #verification
Formal Verification of a Combination Decision Procedure (JF, NS), pp. 347–362.
FME-2002-Shankar #proving
Little Engines of Proof (NS), pp. 1–20.
LICS-2002-Shankar #proving
Little Engines of Proof (NS), p. 3–?.
Combining Shostak Theories (NS, HR), pp. 1–18.
CAV-2001-FilliatreORS #named
ICS: Integrated Canonizer and Solver (JCF, SO, HR, NS), pp. 246–249.
Deconstructing Shostak (HR, NS), pp. 19–28.
LOPSTR-2001-Shankar #functional #static analysis
Static Analysis for Safe Destructive Updates in a Functional Language (NS), pp. 1–24.
TACAS-2001-TiwariRSS #generative #invariant
A Technique for Invariant Generation (AT, HR, HS, NS), pp. 113–127.
Abstract and Model Check While You Prove (HS, NS), pp. 443–454.
FM-1998-OwreRSS #case study #experience #named
PVS: An Experience Report (SO, JMR, NS, DWJSC), pp. 338–345.
TACAS-1997-OwreRS #integration #model checking
Integration in PVS: Tables, Types, and Model Checking (SO, JMR, NS), pp. 366–383.
CADE-1996-CyrlukLS #on the
On Shostak’s Decision Procedure for Combinations of Theories (DC, PL, NS), pp. 463–477.
CAV-1996-OwreRRSS #model checking #named #proving #specification
PVS: Combining Specification, Proof Checking, and Model Checking (SO, SR, JMR, NS, MKS), pp. 411–414.
CAV-1996-RuessSS #composition #verification
Modular Verification of SRT Division (HR, NS, MKS), pp. 123–134.
FME-1996-HavelundS #model checking #protocol #proving #theorem proving #verification
Experiments in Theorem Proving and Model Checking for Protocol Verification (KH, NS), pp. 662–681.
CAV-1995-RajanSS #automation #integration #model checking #proving
An Integration of Model Checking with Automated Proof Checking (SR, NS, MKS), pp. 84–97.
LICS-1995-LincolnSS #higher-order #linear #logic #problem
Decision Problems for Second-Order Linear Logic (PL, AS, NS), pp. 476–485.
LICS-1994-LincolnS #calculus #first-order #linear #logic #proving
Proof Search in First-Order Linear Logic and Other Cut-Free Sequent Calculi (PL, NS), pp. 282–291.
CAV-1993-Shankar #realtime #using #verification
Verification of Real-Time Systems Using PVS (NS), pp. 280–291.
FME-1993-OwreRSH #architecture #fault tolerance #lessons learnt #verification
Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned (SO, JMR, NS, FWvH), pp. 482–500.
CADE-1992-OwreRS #named #prototype #verification
PVS: A Prototype Verification System (SO, JMR, NS), pp. 748–752.
CADE-1992-Shankar #calculus #proving
Proof Search in the Intuitionistic Sequent Calculus (NS), pp. 522–536.
Linearizing Intuitionistic Implication (PL, AS, NS), pp. 51–62.
CADE-2017-BonacinaGS #modulo theories #satisfiability
Satisfiability Modulo Theories and Assignments (MPB, SGL, NS), pp. 42–59.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.