Travelled to:1 × Croatia
1 × Cyprus
1 × Hungary
1 × New Zealand
1 × Poland
1 × The Netherlands
2 × Austria
2 × France
2 × Germany
2 × Portugal
3 × Italy
5 × USA
8 × United Kingdom
Collaborated with:D.Kröning E.M.Clarke G.Fedyukovich A.Tsitovich F.Alberti S.Ghilardi S.Chaki J.C.Browne A.E.J.Hyvärinen O.Sery C.M.Wintersteiger R.Bruttomesso S.F.Rollini S.Tonetta H.Jain D.Peled N.Sinha S.Ranise J.Ouaknine M.Marescotti N.Blanc C.Braghin K.Barone-Adesi B.Cook R.P.Kurshan A.Gurfinkel H.Chockler A.C.D'Iddio E.Pek J.Ivers K.C.Wallnau K.Yorav L.Mariani A.Muhammad A.Ivrii A.Matsliah J.Aldrich M.Barnett D.Giannakopoulou G.T.Leavens P.Jancík L.Alt A.E.J.Hyvärinen J.Kofron F.Pastore S.Sehestedt O.Grumberg T.Touili H.Veith G.Denaro M.Ling M.Oriol A.Rajan M.Tautschnig
Talks about:verif (8) abstract (7) softwar (6) analysi (5) model (5) predic (4) check (4) base (4) properti (3) verilog (3)
Person: Natasha Sharygina
DBLP: Sharygina:Natasha
Facilitated 1 volumes:
EdContributed to:
2015
2015
2014
2014
2014
2013
2013201320122012201120102010
200920092008
2007
2007
2007200720062005
2005
200520052005200420032001200120162016Wrote 34 papers:
- FASE-2015-FedyukovichDHS #bound #dependence #detection #model checking
- Symbolic Detection of Assertion Dependencies for Bounded Model Checking (GF, ACD, AEJH, NS), pp. 186–201.
- SAT-2015-HyvarinenMS #clustering #smt
- Search-Space Partitioning for Parallelizing SMT Solvers (AEJH, MM, NS), pp. 369–386.
- ISSTA-2014-PastoreMHFSSM #testing
- Verification-aided regression testing (FP, LM, AEJH, GF, NS, SS, AM), pp. 37–48.
- SMT-2014-AlbertiGS #array
- Decision Procedures for Flat Array Properties (FA, SG, NS), p. 51.
- TACAS-2014-AlbertiGS #array
- Decision Procedures for Flat Array Properties (FA, SG, NS), pp. 15–30.
- CSMR-2013-ChocklerDLFHMMORSST #named #validation
- PINCETTE — Validating Changes and Upgrades in Networked Software (HC, GD, ML, GF, AEJH, LM, AM, MO, AR, OS, NS, MT), pp. 461–464.
- SAC-2013-ChocklerIMRS #satisfiability #using
- Using cross-entropy for satisfiability (HC, AI, AM, SFR, NS), pp. 1196–1203.
- TACAS-2013-FedyukovichSS #c #incremental #named
- eVolCheck: Incremental Upgrade Checker for C (GF, OS, NS), pp. 292–307.
- CAV-2012-AlbertiBGRS #abstraction #array #named #smt
- SAFARI: SMT-Based Abstraction for Arrays with Interpolants (FA, RB, SG, SR, NS), pp. 679–685.
- CAV-2012-RolliniSS #model checking
- Leveraging Interpolant Strength in Model Checking (SFR, OS, NS), pp. 193–209.
- SMT-2012-AlbertiBGRS #library #modulo theories #reachability
- Reachability Modulo Theory Library (FA, RB, SG, SR, NS), pp. 67–76.
- TACAS-2011-TsitovichSWK #analysis #summary #termination
- Loop Summarization and Termination Analysis (AT, NS, CMW, DK), pp. 81–95.
- CAV-2010-KroeningSTW #analysis #composition #invariant #termination
- Termination Analysis with Compositional Transition Invariants (DK, NS, AT, CMW), pp. 89–103.
- TACAS-2010-BruttomessoPST
- The OpenSMT Solver (RB, EP, NS, AT), pp. 150–153.
- ASE-2009-KroeningSTTW #named #source code
- Loopfrog: A Static Analyzer for ANSI-C Programs (DK, NS, ST, AT, CMW), pp. 668–670.
- SAC-2009-SharyginaTT #abstraction #performance #precise #verification
- The synergy of precise and fast abstractions for program verification (NS, ST, AT), pp. 566–573.
- TACAS-2008-BlancKS #analysis #modelling #named
- Scoot: A Tool for the Analysis of SystemC Models (NB, DK, NS), pp. 467–470.
- DATE-2007-KroeningS #image #interactive #proving #refinement #using #word
- Interactive presentation: Image computation and predicate refinement for RTL verilog using word level proofs (DK, NS), pp. 1325–1330.
- ESEC-FSE-2007-AldrichBGLS #component #specification #verification
- Specification and verification of component-based systems 2007 (JA, MB, DG, GTL, NS), pp. 609–610.
- IFM-2007-BraghinSB #automation #mobile #policy #security #verification
- Automated Verification of Security Policies in Mobile Code (CB, NS, KBA), pp. 37–53.
- TACAS-2007-JainKSC #abstraction #named #refinement
- VCEGAR: Verilog CounterExample Guided Abstraction Refinement (HJ, DK, NS, EMC), pp. 583–586.
- TACAS-2006-KroeningS #approximate #image #logic
- Approximating Predicate Images for Bit-Vector Logic (DK, NS), pp. 242–256.
- CAV-2005-ChakiISW #framework #reasoning
- The ComFoRT Reasoning Framework (SC, JI, NS, KCW), pp. 164–169.
- CAV-2005-CookKS #named #proving #theorem proving #verification
- Cogent: Accurate Theorem Proving for Program Verification (BC, DK, NS), pp. 296–300.
- DAC-2005-JainKSC #abstraction #refinement #verification #word
- Word level predicate abstraction and refinement for verifying RTL verilog (HJ, DK, NS, EMC), pp. 445–450.
- FM-2005-SharyginaCCS #analysis #component
- Dynamic Component Substitutability Analysis (NS, SC, EMC, NS), pp. 512–528.
- IFM-2005-ChakiCGOSTV #specification #verification
- State/Event Software Verification for Branching-Time Specifications (SC, EMC, OG, JO, NS, TT, HV), pp. 53–69.
- TACAS-2005-ClarkeKSY #abstraction #named #satisfiability
- SATABS: SAT-Based Predicate Abstraction for ANSI-C (EMC, DK, NS, KY), pp. 570–574.
- IFM-2004-ChakiCOSS #model checking
- State/Event-Based Software Model Checking (SC, EMC, JO, NS, NS), pp. 128–147.
- FASE-2003-SharyginaB #abstraction #model checking
- Model Checking Software via Abstraction of Loop Transitions (NS, JCB), pp. 325–340.
- FASE-2001-SharyginaBK #analysis #design #object-oriented #reliability #verification
- A Formal Object-Oriented Analysis for Software Reliability: Design for Verification (NS, JCB, RPK), pp. 318–332.
- FME-2001-SharyginaP #approach #reliability #testing #verification
- A Combined Testing and Verification Approach for Software Reliability (NS, DP), pp. 611–628.
- FASE-2016-JancikAFHKS #named
- PVAIR: Partial Variable Assignment InterpolatoR (PJ, LA, GF, AEJH, JK, NS), pp. 419–434.
- CAV-2016-FedyukovichGS #equivalence #simulation
- Property Directed Equivalence via Abstract Simulation (GF, AG, NS), pp. 433–453.