Prof. Natasha Sharygina
Universita della Svizzera Italiana (University of Lugano)
Informatics Department
Carnegie Mellon University
School of Computer Science
Via G. Buffi 13
Lugano, 6900, Switzerland
natasha.sharygina@unisi.ch
natalie@cs.cmu.edu
+41 (0)58 66 64299
+41 (0)58 66 64536 (FAX)
My research interests are in software and hardware verification (e.g. Model-checking, Abstract Interpretation, Decision Procedures for first-order theories, Satisfiability Modulo Theories (SMT)), information security, and concurrent and distributed computing.
Research of my group is supported by Swiss National Science Foundation, Foundation Tasso, Hasler Foundation and EU Cost Initiative.
Software Security (e.g., automated verification of security policies of mobile code; detection of security vulnerabilities) System Modeling and Specification Logics (e.g., state/event-based software model checking) Automated Analysis of Evolving Systems (e.g., component compatibility and substitutability) Formal Verification via Boolean and Theory Reasoning (SMT) (e.g., SAT/SMT-based model checking) Description of ongoing projects can be found here
OpenSMT: Open source SMT solver
SATABS : Model checker for C programs
ComFoRT: Formal reasoning framework for analysis of component-based designs
ObjectCheck : Toolset for Design and Analysis of Object-Oriented Programs
Specification and Verification of Component-based Systems (SAVCBS), 2001 - 2009
USI-CMU Summer School on Dependable Software Systems, 2006 - 2008
Alpine Verification Workshop, 2006 - 2008
A Scalable Decision Procedure for Fixed-Width Bit-Vectors will appear in ICCAD'09
Loopfrog: A Static Analyzer for ANSI-C Programs will appear in ASE'09
OpenSMT 0.2 System Description is in SMT'09
The synergy of precise and fast abstractions for program verification is in ACM SAC'09
Loop Summarization using Abstract Transformers is in ATVA'08
Scoot: A Tool for the Analysis of SystemC Models is in TACAS'08
Verification of Boolean programs with unbounded thread creation in Theoretical Computer Science Journal
Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog is in appear in IEEE TCAD 2008
Automated Verification of Security Policies in Mobile Code in IFM'07
Image Computation and Predicate Refinement for RTL Verilog using Word Level Proofs in DATE'07
VCEGAR: Verilog CounterExample Guided Abstraction Refinement in TACAS'07
Model Checking with Abstraction for Web Services, a book chapter in Test and Analysis of Web Services Springer-Verlag, 2007
Service:
FMCAD (PC co-chair), Formal Methods in Computer-Aided Design Conference, Lugano, Switzerland, October 2010
CAV, Computer-Aided Verification Conference, Edinburgh, UK, July 2010
MEMOCODE Conference, Grenoble, France, July 2010
USI-CMU Summer School on Dependable Computer Systems, Lugano, Switzerland, on-going
St. Petersburg Department of Steklov Institute of Mathematics, Computer Science Club (In Russian), St. Petersburg, Russia, on-going
Undergraduate class on Theory of Computation , 2008, 2009, 2010
Graduate class on Software Verification and Security , 2007
Graduate seminar on Current Research Issues on Formal Reasoning , 2006
Undergraduate class on Software Design (co-instructor with Prof. Alex Wolf), 2006
Consultant, Bell Labs, Computing Sciences Research, Lucent, 2000--2001
Ph.D., The University of Texas at Austin, 2002