Travelled to:1 × Austria
1 × Cyprus
1 × Denmark
1 × Estonia
1 × Finland
1 × Germany
1 × Italy
1 × Portugal
1 × Russia
1 × South Africa
1 × United Kingdom
13 × USA
6 × France
Collaborated with:R.E.Bryant W.Li D.J.Fremont S.Jha S.K.Lahiri S.Qadeer D.E.Holcomb B.A.Brady A.Desai S.Jha O.Strichman S.Mitra T.Dreossi D.Sadigh S.S.Sastry A.L.Sangiovanni-Vincentelli ∅ J.Kotker R.S.0001 S.K.Rajamani D.King T.Jaeger D.Kröning J.Ouaknine M.Vazquez-Chanlatte W.Zheng A.Solar-Lezama L.Tancau R.Bodík V.A.Saraswat R.Ehlers H.Kress-Gazit A.Forin N.Nicolici R.Limaye C.Flanagan E.S.Kim M.Arcak K.Subramani S.Ghosh A.Puggelli S.Gulwani A.Tiwari R.K.Shyamasundar A.K.Bhattacharjee S.D.Dhodapkar J.V.Deshmukh X.Jin M.N.Rabe L.Tentrup C.Rasmussen A.Phanishayee D.Broman J.C.Eidson S.Chakraborty K.S.Meel M.Y.Vardi T.H.Feng L.Wang S.Kanajan V.Ganapathy T.W.Reps D.Muthukumaran M.D.Natale P.Giusto G.Arnold Xiangyu Yue E.Kim H.Ravanbakhsh M.Costa A.Lal N.P.Lopes K.Vaswani
Talks about:verif (9) system (8) base (7) time (6) synthesi (5) abstract (5) program (5) arithmet (4) analysi (4) procedur (3)
Person: Sanjit A. Seshia
DBLP: Seshia:Sanjit_A=
Facilitated 1 volumes:
EdContributed to:
2015
2015
2015
2015
20142014
2014201320122011
201120112010
2010
201020092009
20082007
20072007
2006
200520052004
2004200320032002
199920172017201820182019
2018201620192007Wrote 49 papers:
- CAV-2015-DesaiSQBE #abstraction #approximate #distributed
- Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems (AD, SAS, SQ, DB, JCE), pp. 429–448.
- DAC-2015-SeshiaSS #formal method
- Formal methods for semi-autonomous driving (SAS, DS, SSS), p. 5.
- ESEC-FSE-2015-DesaiQS #testing
- Systematic testing of asynchronous reactive systems (AD, SQ, SAS), pp. 73–83.
- TACAS-2015-ChakrabortyFMSV #generative #on the #parallel #satisfiability #scalability
- On Parallel Scalable Uniform SAT Witness Generation (SC, DJF, KSM, SAS, MYV), pp. 304–319.
- SMT-2014-FremontS #program analysis #smt
- Speeding Up SMT-Based Quantitative Program Analysis (DJF, SAS), pp. 3–13.
- TACAS-2014-LiSSS #synthesis
- Synthesis for Human-in-the-Loop Control Systems (WL, DS, SSS, SAS), pp. 470–484.
- VMCAI-2014-EhlersSK #identifier #synthesis
- Synthesis with Identifiers (RE, SAS, HKG), pp. 415–433.
- CAV-2013-PuggelliLSS #nondeterminism #polynomial #verification
- Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties (AP, WL, ALSV, SAS), pp. 527–542.
- DAC-2012-LiSJ #crowdsourcing #named #towards #verification
- CrowdMine: towards crowdsourced human-assisted verification (WL, SAS, SJ), pp. 1254–1255.
- DAC-2012-Seshia #deduction #induction #named #synthesis #verification
- Sciduction: combining induction, deduction, and structure for verification and synthesis (SAS), pp. 356–365.
- DAC-2011-HolcombBS #performance #verification
- Abstraction-based performance verification of NoCs (DEH, BAB, SAS), pp. 492–497.
- DATE-2011-BradyHS
- Counterexample-guided SMT-driven optimal buffer sizing (BAB, DEH, SAS), pp. 329–334.
- TACAS-2011-SeshiaK #analysis #named #tool support
- GameTime: A Toolkit for Timing Analysis of Software (SAS, JK), pp. 388–392.
- DAC-2010-LiFS #mining #scalability #specification #verification
- Scalable specification mining for verification and diagnosis (WL, AF, SAS), pp. 755–760.
- DAC-2010-MitraSN #challenge #validation
- Post-silicon validation opportunities, challenges and recent advances (SM, SAS, NN), pp. 12–17.
- ESOP-2010-KingJMJJS #automation #security
- Automating Security Mediation Placement (DK, SJ, DM, TJ, SJ, SAS), pp. 327–344.
- ICSE-2010-JhaGST #component #synthesis
- Oracle-guided component-based program synthesis (SJ, SG, SAS, AT), pp. 215–224.
- CAV-2009-JhaLS #named #performance #smt
- Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic (SJ, RL, SAS), pp. 668–674.
- DATE-2009-HolcombLS #analysis #design #fault
- Design as you see FIT: System-level soft error analysis of sequential circuits (DEH, WL, SAS), pp. 785–790.
- DATE-2009-LiNZGSS #dependence #optimisation #protocol
- Optimizations of an application-level protocol for enhanced dependability in FlexRay (WL, MDN, WZ, PG, ALSV, SAS), pp. 1076–1081.
- FSE-2008-KingJJS #data flow #effectiveness
- Effective blame for information-flow violations (DK, TJ, SJ, SAS), pp. 250–260.
- DATE-2007-FengWZKS #automation #black box #generative #interactive #realtime
- Interactive presentation: Automatic model generation for black box real-time systems (THF, LW, WZ, SK, SAS), pp. 930–935.
- DATE-2007-SeshiaLM #fault
- Verification-guided soft error resilience (SAS, WL, SM), pp. 1442–1447.
- PLDI-2007-Solar-LezamaATBSS #sketching
- Sketching stencils (ASL, GA, LT, RB, VAS, SAS), pp. 167–178.
- TACAS-2007-BryantKOSSB #abstraction
- Deciding Bit-Vector Arithmetic with Abstraction (REB, DK, JO, SAS, OS, BAB), pp. 358–372.
- ASPLOS-2006-Solar-LezamaTBSS #combinator #finite #sketching #source code
- Combinatorial sketching for finite programs (ASL, LT, RB, SAS, VAS), pp. 404–415.
- CADE-2005-BryantS #verification
- Decision Procedures Customized for Formal Verification (REB, SAS), pp. 255–259.
- ICSE-2005-GanapathySJRB #automation
- Automatic discovery of API-level exploits (VG, SAS, SJ, TWR, REB), pp. 312–321.
- CAV-2004-KroeningOSS #satisfiability
- Abstraction-Based Satisfiability Solving of Presburger Arithmetic (DK, JO, SAS, OS), pp. 308–320.
- CAV-2004-LahiriS
- The UCLID Decision Procedure (SKL, SAS), pp. 475–478.
- LICS-2004-SeshiaB #bound #quantifier #using
- Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds (SAS, REB), pp. 100–109.
- CAV-2003-SeshiaB #automaton #bound #model checking #using
- Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods (SAS, REB), pp. 154–166.
- DAC-2003-SeshiaLB #hybrid #logic #satisfiability
- A hybrid SAT-based decision procedure for separation logic with uninterpreted functions (SAS, SKL, REB), pp. 425–430.
- CAV-2002-BryantLS #logic #modelling #using #verification
- Modeling and Verifying Systems Using a Logic of Counter Arithmetic with λ Expressions and Uninterpreted Functions (REB, SKL, SAS), pp. 78–92.
- CAV-2002-FlanaganQS #composition #parallel #source code #thread
- A Modular Checker for Multithreaded Programs (CF, SQ, SAS), pp. 180–194.
- CAV-2002-StrichmanSB #satisfiability
- Deciding Separation Formulas with SAT (OS, SAS, REB), pp. 209–222.
- FM-v2-1999-SeshiaSBD
- A Translation of Statecharts to Esterel (SAS, RKS, AKB, SDD), pp. 983–1007.
- ESEC-FSE-2017-0001RS #compilation #verification
- A compiler and verifier for page access oblivious computation (RS0, SKR, SAS), pp. 649–660.
- CAV-2017-Vazquez-Chanlatte #clustering #learning #logic
- Logical Clustering and Learning for Time-Series Data (MVC, JVD, XJ, SAS), pp. 305–325.
- CAV-2018-DreossiJS #learning #semantics
- Semantic Adversarial Deep Learning (TD, SJ, SAS), pp. 3–26.
- CAV-2018-FremontS
- Reactive Control Improvisation (DJF, SAS), pp. 307–326.
- CAV-2018-RabeTRS #comprehension #incremental
- Understanding and Extending Incremental Determinization for 2QBF (MNR, LT, CR, SAS), pp. 256–274.
- CAV-2019-DreossiFGKRVS #analysis #design #named #tool support
- VerifAI: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems (TD, DJF, SG, EK, HR, MVC, SAS), pp. 432–442.
- CAV-2019-KimAS #flexibility #pipes and filters #robust #synthesis
- Flexible Computational Pipelines for Robust Abstraction-Based Control Synthesis (ESK, MA, SAS), pp. 591–608.
- OOPSLA-2018-DesaiPQS #composition #distributed #programming #testing
- Compositional programming and testing of dynamic distributed systems (AD, AP, SQ, SAS), p. 30.
- PLDI-2016-0001CLLRSV #design #verification
- A design and verification methodology for secure isolated regions (RS0, MC, AL, NPL, SKR, SAS, KV), pp. 665–681.
- PLDI-2019-FremontDGYSS #generative #named #specification
- Scenic: a language for scenario specification and scene generation (DJF, TD, SG, XY, ALSV, SAS), pp. 63–78.
- SMT-J-2006-SeshiaSB #constraints #on the
- On Solving Boolean Combinations of UTVPI Constraints (SAS, KS, REB), pp. 67–90.