The full list of recent papers (2015 - 2011) can be
found here
-
A Model Checking-based Approach for Security Policy Verification of Mobile Systems,
Braghin, C.; Sharygina, N.; Barone-Adesi, K., Formal Aspects of Computing Journal (FACJ), Springer Verlag, to appear, DOI: 10.1007/s00165-010-0159-y
Download:
bsb_facj2010.pdf
-
A Flexible Schema for Generating Explanations in Lazy Theory Propagation,
Bruttomesso, R.; Pek, E.; Sharygina, N., International Conference on Formal Methods and Models for Codesign (MEMOCODE), Grenoble, France
Download:
bps_memocode2010.pdf
-
An Efficient and Flexible Approach to Resolution Proof Reduction,
Rollini, S.F.; Bruttomesso, R.; Sharygina, N., Haifa Verification Conference (HVC) 2010, Haifa, Israel
Download:
rbs10.pdf
-
Flexible Interpolation with Local Proof Transformations,
Bruttomesso, R.; Rollini, S.F.; Sharygina, N.; Tsitovich, A., International Conference of Computer Aided Design (ICCAD), San Jose, USA
Download:
brst10.pdf
-
The OpenSMT Solver,
Bruttomesso, R.; Pek, E.; Sharygina, N.; Tsitovich, A., International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Volume 6015, Paphos, Cyprus, p.150-153
Download:
bpst2010.pdf
-
Termination Analysis with Compositional Transition Invariants,
Kroening, D.; Sharygina, N.; Tsitovich, A.; Wintersteiger, C.M., International Conference on Computer-Aided Verification (CAV), Edinburgh, UK, p.89-103
Download:
kstw2010.pdf
-
A Scalable Decision Procedure for Fixed-Width Bit-Vectors,
Bruttomesso, R.; Sharygina, N., International Conference of Computer Aided Design (ICCAD), San Jose (CA)
Download:
iccad09.pdf
-
Loopfrog: A Static Analyzer for ANSI-C Programs,
Kroening, D.; Sharygina, N.; Tonetta, S.; Tsitovich, A.; Wintersteiger, C.M., The 24th IEEE/ACM International Conference on Automated Software Engineering, Auckland, New Zealand, p.668-670
Download:
main.pdf
-
The Synergy of Precise and Fast Abstractions for Program Verification,
Sharygina, N.; Tonetta, S.; Tsitovich, A., 24th Annual ACM Symposium on Applied Computing (SAC), Honolulu, USA, p.566-573
Download:
stt2009.pdf
-
Loop Summarization using Abstract Transformers,
Kroening, D.; Sharygina, N.; Tonetta, S.; Tsitovich, A.; Wintersteiger, C.M., 6th International Symposium on Automated Technology for Verification and Analysis (ATVA), Volume 5311, Seoul, South Korea, p.111-125
Download:
ksttw08.pdf
-
Scoot: A Tool for the Analysis of SystemC Models,
Blanc, N.; Kroening, D.; Sharygina, N., TACAS, p.467-470
Download:
BlancKS08.pdf
-
Verification of evolving software via component substitutability analysis,
Chaki, S.; Clarke, E.M.; Sharygina, N.; Sinha, N., Formal Methods in System Design, Volume 32, Number 3, p.235-266
Download:
ChakiCSS08.pdf
-
Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog,
Jain, H.; Kroening, D.; Sharygina, N.; Clarke, E.M., IEEE Trans. on CAD of Integrated Circuits and Systems, Volume 27, Number 2, p.366-379
Download:
JainKSC08.pdf
-
Automated Verification of Security Policies in Mobile Code,
Braghin, C.; Sharygina, N.; Barone-Adesi, K., Integrated Formal Methods (IFM), LNCS, Spinger, Volume 4591, p.37-53
-
Image computation and predicate refinement for RTL verilog using word level proofs,
Kroening, D.; Sharygina, N., DATE, p.1325-1330
-
Automated Verification of Boolean Programs with Unbounded Thread Creation, B. Cook, D. Kroening and N. Sharygina, Journal of Theoretical Computer Science (TCS), Vol. 388,
Elsevier, pp. 227 - 242.
-
VCEGAR: Verilog CounterExample Guided Abstraction Refinement,
Jain, H.; Kroening, D.; Sharygina, N.; Clarke, E.M., Lecture Notes in Computer Science, Volume 4424, p.583-586
Download:
vcegar-tool.pdf
-
Model Checking with Abstraction for Web Services,
Sharygina, N.; Kröning, D., Test and Analysis of Web Services, p.121-145
- Over-Approximating Boolean Programs with Unbounded Thread Creation, B. Cook, D. Kroening, and N. Sharygina, Proceedings of the Formal Methods in Computer-Aided
Design Conference (FMCAD), IEEE Computer Society Press, pp. 53 - 59.
-
Approximating Predicate Images for Bit-Vector Logic, D. Kroening, and N. Sharygina, Pro-
ceedings of the Tools and Algorithms for the Construction and Analysis of Systems Conference
(TACAS), Lecture Notes in Computer Science, Vol. 3920, Springer-Verlag, pp. 242 -
256
-
Dynamic Component Substitutability
Analysis, Sharygina, N., Chaki S., Clarke, E., and Sinha, N., In Proceedings of the Formal Methods (FM) 2005 conference, Lecture Notes in Computer Science,
Springer-Verlag, Vol. 3582, pp. 512 - 528
-
The ComFoRT Reasoning Framework, Chaki, S., Ivers, J., Sharygina, N., and Wallnau, K.,
In Proceedings of the Computer-Aided Verification (CAV) 2005 conference , Springer, LNCS, Vol. 3576, pp. 164 - 169
-
COGENT: Accurate Theorem Proving for
Program Verification, Cook, B., Kroening, D., and Sharygina, N., In Proceedings of the
Computer-Aided Verification (CAV) 2005 conference, Lecture Notes in
Computer Science, Vol. 3576, Springer, pp. 296 - 300
-
Symbolic Model Checking for
Asynchronous Boolean Programs, Cook, B., Kroening, D., and Sharygina, N., In Proceedings of the 12th International SPIN Workshop on Model Checking of Software, Lecture Notes in Computer Science,
Springer-Verlag, Vol. 3639, pp. 75 - 90
-
SATABS: SAT-based Predicate
Abstraction for ANSI-C , E. Clarke, D. Kroening, N. Sharygina, and K. Yorav,
In proceedings of TACAS (Tools and Algorithms for the
Construction and Analysis of Systems) 2005 International Conference, Lecture Notes in Computer Science, Springer, Vol. 3440, p. 570
- 574
-
Predicate Abstraction and Refinement
Techniques for Verifying Verilog , H. Jian, D. Kroening, N. Sharygina, and E. Clarke, In Proceedings
of the
DAC (Design and Automation) 2005 International Conference, ACM Press, ISBN 1-59593-058-2, pp. 445 - 450. This paper was nominated for the
best paper award of the DAC’05 conference, 16 out of 151 accepted papers were
nominated
-
State/event Software Verification for Branching Time Specifications, S. Chaki, E. Clarke, O. Grumberg, J. Ouaknine, N. Sharygina, T. Touili, and H. Veith,
, In Proceedings of
Integrated Formal Methods Conference (IFM), Lecture Notes in Computer Science, Springer-Verlag, Vol.
3771, pp. 53 - 69.
-
Formal Verification of SystemC by Automatic Hardware-
Software Partitioning, D. Kroening, and N. Sharygina, Proceedings of the
3rd ACM-IEEE International Conference on Formal
Methods and Models for Co-design (MEMOCODE), IEEE Press, pp. 101 - 110.
-
Automated, compositional and
iterative deadlock detection, S. Chaki, E. Clarke, J. Ouaknine, N. Sharygina, and N. Sinha,
In Proceedings of the Second ACM-IEEE International
Conference on Formal Methods for Codesign (MEMOCODE) 2004, IEEE Press,
pp. 201-210.
-
Verification of Evolving Software, S. Chaki, N. Sharygina, and N. Sinha, In Proceedings of the Specification and Verification of
Component-based Systems (SAVCBS) Workshop
-
Overview of ComFoRT, A Model
Checking Reasoning Framework, J. Ivers, and N. Sharygina, Carnegie Mellon
University, Software Engineering Institute publications,
CMU/SEI-2004-TN-0181
-
State/Event-based Software Model Checking, S. Chaki, E. Clarke, J. Ouaknine, N. Sharygina, and N. Sinha, In Proceedings of IFM (Integrated Formal Methods) 2004 International Conference,
Lecture Notes in Computer Science 2999, Springer, p. 128 - 147. This
paper was nominated for the BCS-FACS best paper award
-
Predicate Abstraction of ANSI-C Programs using SAT, E. Clarke, D. Kroening, N. Sharygina, and K. Yorav, In the
Formal Methods in System Design Journal, Vol. 25(2), p. 105 - 127.
A conference version of the paper first appeared in the Proceedings of the Model Checking for Dependable Software-Intensive Systems Workshop of
the International Conference on Dependable Systems and Networks 2003
-
Lessons Learned from Model Checking
a NASA Robot Controller , N. Sharygina, J. Browne, R. Kurshan, V. Levin, and Fei Xie, In the Formal Methods in System Design Journal , Vol. 25(3), p. 241 - 270. The paper was
first presented at the SEI Software Model Checking Workshop, Pittsburgh, PA, USA, March, 2003
-
A Combined Testing and Verification Approach
for Software Reliability, N. Sharygina, and D. Peled, In the FME 2001: Formal Methods for Increasing Software Productivity: International Symposium of Formal Methods Europe, Berlin, Germany, March 12-16, 2001,
Lecture Notes in Computer Science, Springer, Vol. 2021, p. 611 - 628
-
A Formal Object-Oriented Analysis for Software Reliability, N. Sharygina, and J. Browne, In the Fundamental Approaches to Software Engineering : 4th International Conference, FASE 2001, Lecture Notes in Computer Science, Springer, Vol. 2029, p. 318 - 322