The following pages link to Natasha Sharygina (Q287271):
Displaying 49 items.
- Decision procedures for flat array properties (Q287272) (← links)
- A model checking-based approach for security policy verification of mobile systems (Q432137) (← links)
- Resolution proof transformation for compression and interpolation (Q479815) (← links)
- An extension of lazy abstraction with interpolation for programs with arrays (Q479820) (← links)
- A cooperative parallelization approach for property-directed \(k\)-induction (Q784140) (← links)
- Verification of evolving software via component substitutability analysis (Q934712) (← links)
- Lattice-based refinement in bounded model checking (Q1629959) (← links)
- Theory refinement for program verification (Q1680264) (← links)
- Predicate abstraction of ANSI-C programs using SAT (Q1888196) (← links)
- Exploiting partial variable assignment in interpolation-based model checking (Q2009611) (← links)
- Farkas-based tree interpolation (Q2233543) (← links)
- Loop summarization using state and transition invariants (Q2248058) (← links)
- Concurrent software verification with states, events, and deadlocks (Q2432214) (← links)
- Verification of Boolean programs with unbounded thread creation (Q2464944) (← links)
- (Q2764005) (← links)
- (Q2764134) (← links)
- Towards Completeness in Bounded Model Checking Through Automatic Recursion Depth Detection (Q2797866) (← links)
- OpenSMT2: An SMT Solver for Multi-core and Cloud Computing (Q2818042) (← links)
- Definability of Accelerated Relations in a Theory of Arrays and Its Applications (Q2849479) (← links)
- PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification (Q2870162) (← links)
- Lazy Abstraction with Interpolants for Arrays (Q2891439) (← links)
- A New Acceleration-Based Combination Framework for Array Properties (Q2964461) (← links)
- Loop Summarization and Termination Analysis (Q3000639) (← links)
- Modeling for Verification (Q3176361) (← links)
- Search-Space Partitioning for Parallelizing SMT Solvers (Q3453241) (← links)
- Booster: An Acceleration-Based Verification Framework for Array Programs (Q3457775) (← links)
- Automated Discovery of Simulation Between Programs (Q3460090) (← links)
- Loop Summarization Using Abstract Transformers (Q3540068) (← links)
- Program Compatibility Approaches (Q3591398) (← links)
- (Q4417841) (← links)
- Property Directed Equivalence via Abstract Simulation (Q4633561) (← links)
- Interpolation Properties and SAT-Based Model Checking (Q5166692) (← links)
- Function Summarization Modulo Theories (Q5222945) (← links)
- Lookahead-Based SMT Solving (Q5222970) (← links)
- SMTS: Distributed, Visualized Constraint Solving (Q5222977) (← links)
- eVolCheck: Incremental Upgrade Checker for C (Q5326332) (← links)
- An Efficient and Flexible Approach to Resolution Proof Reduction (Q5391528) (← links)
- Model Checking Software (Q5394555) (← links)
- State/Event Software Verification for Branching-Time Specifications (Q5429308) (← links)
- Tools and Algorithms for the Construction and Analysis of Systems (Q5703792) (← links)
- Computer Aided Verification (Q5716552) (← links)
- Computer Aided Verification (Q5716570) (← links)
- FM 2005: Formal Methods (Q5716900) (← links)
- Tools and Algorithms for the Construction and Analysis of Systems (Q5899062) (← links)
- Integrated Formal Methods (Q5901610) (← links)
- SMT-based verification of program changes through summary repair (Q6056638) (← links)
- Symbolic model checking for TLA+ made faster (Q6535348) (← links)
- The \textsc{Golem} Horn solver (Q6535535) (← links)
- Transition power abstractions for deep counterexample detection (Q6535576) (← links)
