Latest News

Documents & Publications

Background Publications

[A87]

Dana Angluin. Learning regular sets from queries and counterexamples. In Information and Computation, volume 75(2), pages 87–106, November 1987.

[AFMUZZ06]

Hezi Azatchi, Laurent Fournier, Eitan Marcus, Shmuel Ur, Avi Ziv, Keren Zohar: Advanced Analysis Techniques for Cross-Product Coverage. IEEE Trans. Computers 55(11): 1367-1379 (2006).

[Ball99]

T. Ball, The Concept of Dynamic Analysis, in proceedings of the joint 7th European Software Engineering Conference and ACM SIGSOFT International Symposium on the Foundations of Software Engineering (ESEC/FSE), 1999.

[BCMDH92]

J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, 1992.

[BFMNU05]

Arkady Bron, Eitan Farchi, Yonit Magid, Yarden Nir, Shmuel Ur. Applications of synchronization coverage. PPOPP 2005: 206-212.

[BNRS08]

Nels Beckman, Aditya V. Nori, Sriram K. Rajamani, and Robert J. Simmons.  Proofs from tests. In Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2008, Seattle, WA, USA, July 20-24, 2008, p. 3--14. ACM, 2008.

[BR00]

T. Ball and S.K. Rajamani. Boolean programs: A model and process for software analysis. Technical Report 2000-14, Microsoft Research, February 2000.

[C96]

Patrick Cousot. Abstract interpretation. Symposium on Models of Programming Languages and Computation, ACM Computing Surveys, 28(2):324–328, 1996.

[CE04]

McCamant and M. D. Ernst. Early identification of incompatibilities in multi-component upgrades. In ECOOP 2004 - Object-Oriented Programming, 18th European Conference, Olso, Norway, 2004.

[CGL92]

E. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. In Principles of Programming Languages, January 1992.

[CGP99]

Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled, Model Checking, MIT Press, 1999, ISBN 0-262-03270-8.

[CHK07]

Dr. Hana Chockler, Joseph Y. Halpern, Orna Kupferman: What causes a system to satisfy a specification? To appear in ACM TOCL, 2007.

[CK02]

Dr. Hana Chockler, Orna Kupferman: Coverage of Implementations by Simulating Specifications. IFIP TCS 2002: Proceedings of the IFIP 17th World Computer Congress-TC1 Stream/2nd IFIP International Conference on Theoretical Computer Science, 409-421.

[CKKV01]

Dr. Hana Chockler, Orna Kupferman, Robert P. Kurshan, Moshe Y. Vardi: A Practical Approach to Coverage in Model Checking. CAV 2001: Proceedings of the 13th International Conference on Computer Aided Verification, 66-78.

[CKP10]

Dr. Hana Chockler, Daniel Kroening, and Mitra Purandare. Coverage in Interpolation-based Model Checking. In Proceedings of DAC 2010.

[CKS04]

Byron Cook, Daniel Kroening, and Natasha Sharygina. Accurate theorem proving for program verification. In Proceedings of ISoLA 2004, volume 4313 of Lecture Notes in Computer Science, pages 96–114. Springer Verlag, 2006.

[CKSY04]

E. M. Clarke, D. Kroening, N. Sharygina, K. Yorav. Predicate abstraction of ANSI-C programs using SAT. In Formal Methods in System Design Journal, Vol. 25(2), p. 107 - 127, September 2004. Kluwer.

[CKSY04]

Edmund Clarke, Daniel Kroening, Natasha Sharygina, and Karen Yorav.   Predicate abstraction of ANSI–C programs using SAT. Formal Methods in System Design (FMSD), 25:105–127, 2004.

[CKSY05]

E. Clarke, D. Kroening, N. Sharygina, and K. Yorav. SATABS: SAT-based predicate abstraction for ANSI-C. In TACAS, LNCS. Springer, 2005.

[CKV06a]

Dr. Hana Chockler, Orna Kupferman, Moshe Y. Vardi: Coverage metrics for temporal logic model checking. Formal Methods in System Design 28(3): 189-212 (2006)

[CKV06b]

Dr. Hana Chockler, Orna Kupferman, Moshe Y. Vardi: Coverage metrics for formal verification. STTT 8(4-5): 373-386 (2006)

[Colin05]

S. Colin and L. Mariani, Run-time Verification, book chapter in Model-based Testing of Reactive Systems, Manfred Broy, Bengt Jonsson, Joost-Pieter Katoen, Martin Leucker and Alexander Pretschner (eds.), LNCS, volume 3472, Springer Verlag, pp 525-556, 2005.

[CT01]

Multithreaded and Networked Programming, T. W. Christopher and G.K. Thiruvathukal, Chapter 3, p. 43, February 2001.

[DKW2008]

V. D’Silva, D. Kroening, G. Weissenbacher. A Survey of Automated Techniques for Formal Software Verification. In IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), p 1165-1178, 2008, IEEE.

[E03]

Michael D. Ernst.  Static and dynamic analysis: Synergy and duality.  In  WODA: ICSE Workshop on Dynamic Analysis, OR, pages 24--27, 2003.

[ECGN01]

Michael Ernst, Jake Cockrell, William G. Griswold, and David Notkin.  Dynamically discovering likely program invariants to support program evolution.   IEEE Transactions on Software Engineering, 27(2):99--123, 2001.

[ECGN99]

M.D. Ernst, J. Cockrell, W.G. Griswold, and D. Notkin. Dynamically discovering likely program invariants to support program evolution. In International Conference on Software Engineering (ICSE’99), pages 213–224, 1999.

[Ernst03]

M.D. Ernst, Static and dynamic analysis: Synergy and duality, ICSE Workshop on Dynamic Analysis (WODA), 2003.

[Fag99]

M.E. Fagan. Design and code inspections to reduce errors in program development. IBM Systems Journal, 38(2-3), Special Issue: Turning Points in Computing 1962-1999.

[GCKS06]

Alex Groce, Sagar Chaki, Daniel Kroening, and Ofer Strichman. Error explanation with distance metrics. Software Tools for Technology Transfer (STTT), 8:229–247, June 2006.

[GFLLUW96]

Daniel Geist, Monica Farkas, Avner Landver, Yossi Lichtenstein, Shmuel Ur, Yaron Wolfsthal: Coverage-Directed Test Generation Using Symbolic Techniques. FMCAD 1996: 143-158

[GHKNR06]

Bhargav S. Gulavani, Thomas A. Henzinger, Yamini Kannan, Aditya V. Nori, and Sriram K. Rajamani.  SYNERGY: a new algorithm for property checking.  In  Proceedings ACM SIGSOFT Symposium on Foundations of Software Engineering, FSE 2005, Portland, Oregon, USA, November 5-11, 2006, pages 117--127. ACM, 2006.

[GHOUZ98]

Raanan Grinwald, Eran Harel, Michael Orgad, Shmuel Ur, Avi Ziv: User Defined Coverage - A Tool Supported Methodology for Design Verification. DAC 1998: 158-163.

[GK04]

Alex Groce and Daniel Kroening: Counterexample Guided Abstraction Refinement via Program Execution. Proceedings of ICFEM 2004, 224-238, LNCS 3308, Springer.

[GK05]

Patrice Godefroid and Nils Klarlund.  Software model checking: Searching for computations in the abstract or the concrete.  In  Integrated Formal Methods, 5th International Conference, IFM 2005, Eindhoven, The Netherlands, 2005, Proceedings, volume 3771 of  LNCS, pages 20--32. Springer, 2005.

[GK05]

Alex Groce and Daniel Kroening. Making the most of BMC counterexamples. In Proceedings of BMC 2004, volume 119 of ENTCS, pages 67–81. Elsevier, 2005.

[GKS05]

Patrice Godefroid, Nils Klarlund, and Koushik Sen.  DART: directed automated random testing.  In  Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, Chicago, IL, USA, June 12-15, 2005. ACM, 2005.

[GLM08]

[GT05]

P. Godefroid, M. Y. Levin, and D. Molnar.  Automated Whitebox Fuzz Testing.  In Proceedings of the Network and Distributed System Security Symposium, 2008.
Penny Grubb and Armstrong Takang . Software Maintenance Concepts and Practices. Second edition, World Scientific, 2005.

[H03]

The Spin Model Checker: Primer and Reference Manual, Addison-Wesley, ISBN 0-321-22862-6, 608 pgs, 2003

[Habib05]

A. Habib, S. Fahmy and B. Bhargava, Monitoring and controlling QoS network domains, International Journal of Network Management, 15 (1), 11-29, John Wiley & Sons, Inc., 2005.

[Hangal02]

S. Hangal and M.s. Lam, Tracking down software bugs using anomaly detection, in proceedings of the 24th International Conference on Software Engineering, IEEE Computer Society, 2002

[HJMS03]

Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre. Software Verification with Blast. In Proceedings of the 10th SPIN Workshop on Model Checking Software (SPIN 2003), LNCS 2648, Springer-Verlag, pages 235–239, 2003.

[IBM]

IBM, Rational Purify Plus, http://www.ibm.com/software/awdtools/purifyplus/.

[Impact]

The Economic Impacts of Inadequate Infrastructure for Software Testing, Special Planning Report 02-03, National Institute of Standards and technology, US Department of Commerce, May 2002 http://www.nist.gov/director/prog-ofc/report02-3.pdf

[Intel]

Intel Accelerates Dual-Core Processor Timetable, Peter Clarke, EE Times, 2005,http://www.eetimes.com/news/latest/showArticle.jhtml?articleID=168601629

[ITER2009a]

ITER web site, www.iter.org

[ITER2009b]

ITER technical basis. Ch. 2.4 Divertor,  www.iter.org/reports.htm

[ITER2009c]

ITER news February 2, 2009, www.iter.org/newsline/issues/67/ITERnewsline.htm

[J77]

Stephen Johnson. Lint, a C program checker. Computer Science Technical Report 65, Bell Laboratories, December 1977.

[Jalote06]

P. Jalote, V. Vangala, T. Singh and P. Jain, Program partitioning: a framework for combining static and dynamic analysis, in proceedings of the ICSE International workshop on Dynamic Analysis, ACM Press, 2006.

[JLPWRFHKR08]

Alexander Jesser, Stefan Lämmermann, Alexander Pacholik, Roland Weiss, Jürgen Ruf, Wolfgang Fengler, Lars Hedrich, Thomas Kropf und Wolfgang Rosenstiel. Advanced Assertion Based Design for Mixed-Signal Verification. IEICE TRANS. FUNDAMENTALS, VOL.E91–A, NO.10: Special Section on VLSI Design and CAD Algorithms, Dezember, 2008, pp. 3548-3555

[Jon00]

Capers Jones. Software assessments, benchmarks, and best practices, Addison-Wesley Information Technology Series, 2000

[Jon98]

Capers Jones. Estimating software costs. McGraw-Hill, 1998.

[JT2007]

Järvenpää, J., Timperi, A., Remote Handling Systems, FUSION Technology Programme 2003-2006. Technology Programme Report 1/2007. TEKES, p. 97-113, http://www.tekes.fi/julkaisut/Fusion.pdf

[Kiczales97]

G. Kiczales, J. Lamping, A. Mendhekar, C. Maeda, C. Lopes, J.-M. Loingtier, and J. Irwin. Aspect-oriented programming, in proceedings of the European Conference on Object-Oriented Programming, volume 1241, pages 220–242. Springer-Verlag, 1997

[KSW09]

E. Kolb, O. Šerý, R. Weiss. Applicability of the BLAST Model Checker: An Industrial Case Study. Submitted for publication, 2009

[KWD09]

Heiko Kozilek, Roland Weiss, Jens Doppelhamer. Evolving Industrial Software Architectures into a Software Product Line: A Case Study.  Fifth International Conference on the Quality of Software Architectures (QoSA 2009), USA.

[Lencev06]

R. Lencevicius and E. Metz, Performance assertions for mobile devices, in proceedings of the 2006 International Symposium on Software Testing and Analysis, ACM Press, 2006.

[LMUZ02]

Oded Lachish, Eitan Marcus, Shmuel Ur, Avi Ziv: Hole analysis for functional coverage data. DAC 2002: 807-812

[Lorenzoli08]

D. Lorenzoli, L. Mariani and M. Pezzè, Automatic Generation of Software Behavioral Models, in proceedings of the 30th International Conference on Software Engineering (ICSE 2008), IEEE Computer Society, 2008.

[Mariani05]

L. Mariani and M. Pezzè, Behaviour Capture and Test: Automated Analysis of Component Integration, in proceedings of the 10th IEEE International Conference on Engineering of Complex Computer Systems, IEEE Computer Society, 2005.

[Mariani07]

L. Mariani, S. Papagiannakis and M. Pezzè, Compatibility and Regression Testing of COTS-component-based Software, In Proceedings of the 29th International Conference on Software Engineering (ICSE 2007), 2007.

[McCama03]

S. McCamant and M.D. Ernst, Predicting problems caused by component upgrades, in proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, ACM Press, 2003.

[NE01] 

Jeremy W. Nimmer and Michael D. Ernst.  Static verification of dynamically detected program invariants: Integrating Daikon and ESC/java.   Electr. Notes Theor. Comput. Sci, 55(2), 2001.

[NI2009]

www.ni.com/info (UTF)

[NRTT09]

Aditya V. Nori, Sriram K. Rajamani, SaiDeep Tetali, , and Aditya V. Thakur.  The Yogi project: Software property checking via static analysis and testing.  In  Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2009.

[Orso01]

A. Orso, G. Vigna and M.J. Harrold, MASSA: Mobile Agents Security through Static/Dynamic Analysis, in proceedings of the ICSE Workshop on Software Engineering and Mobility, 2001.

[PIJ2007]

J. Palmer, M. Irving, J. Järvenpää, H. Mäkinen, H. Saarinen, M. Siuko, A. Timperi, S. Verho. The design and development of divertor remote handling equipment for ITER // Fusion Engineering and Design, 82, 2007, pp. 1977–1982

[PNRWKR06]

Prakash M. Peranandam, Pradeep K. Nalla, Jürgen Ruf, Roland J. Weiss, Thomas Kropf, and Wolfgang Rosenstiel. Fast Falsification Based on Symbolic Bounded Property Checking, 43rd Design Automation Conference (DAC'06), July 24-28, 2006, San Francisco, USA.

[PNWRKR05]

Prakash M. Peranandam, Pradeep K. Nalla, Roland J. Weiss, Jürgen Ruf, Thomas Kropf, and Wolfgang Rosenstiel. Overlap Reduction in Symbolic System Traversal. IEEE International High Level Design Validation and Test Workshop 2005 (HLDVT 05), Napa Valley, California, USA.

[Pro2007]

Progress Towards the Lisbon Objectives in Education and Training – Indicators and Benchmarks, 2007, http://ec.europa.eu/education/policies/2010/progressreport_en.html

[PY07]

M. Pezzè and M. Young, Software Testing and Analysis – Process principles and Techniques, John Wiley, 2007.

[QD]

Quality Development Is Crucial to Emerging Technologies, Gartner Report K-19-8371, April 2003.

[Raz02]

O. Raz, P. Koopman and M. Shaw, Semantic anomaly detection in online data sources, in Proceedings of the 24th International Conference on Software Engineering, ACM Press, 2002.

[Ronen06]

I. Ronen, N. Dor, S. Porat and Y. Dubinsky, Combined static and dynamic analysis for inferring program dependencies using a pattern language, in proceedings of the IBM conference of the Center for Advanced Studies on Collaborative research, ACM Press, 2006.

[RSU02]

Gil Ratsaby, Baruch Sterin, Shmuel Ur: Improvements in Coverability Analysis. FME 2002: 41-56

[RUW01]

Gil Ratzaby, Shmuel Ur, Yaron Wolfsthal: Coverability Analysis Using Symbolic Model Checking. CHARME 2001: 155-160.

[RWKR04]

Jürgen Ruf, Roland J. Weiss, Thomas Kropf, and Wolfgang Rosenstiel. Modeling and Formal Verification of Production Automation Systems. Integration of Software Specification Techniques for Applications in Engineering. Lecture Notes in Computer Science, Vol. 3147, Springer, 2004.

[SAM2008]

[S05]

H. Saarinen, L. Aha, A. Muhammad, J. Mattila, M. Siuko, M. Vilenius et al., Optimized Hardware Design for the Divertor Handling control system, 25th Symposium on Fusion Technology, 15-19 September, 2008, Rostock, Germany
Richard Stuzke. Estimating Software Intensive Systems. 2005, Addison-Wesley.

[Savage97]

S. Savage, M. Burrows, G. Nelson, P. Sobalvarro and T. Anderson, Eraser: a dynamic data race detector for multithreaded programs, ACM Transactions on Computer Systems, 15(4), 1997, 391-411, 1997.

[Sharygina05]

Natasha Sharygina, Sagar Chaki, Edmund M. Clarke, and Nishant Sinha, Dynamic Component Substitutability Analysis, In Proc. of Formal Methods Conference, LNCS 3582, pages 512-528, 2005.

[Sci2006]

Science, pp. 238-242, Oct 13, 2006

[SCIW05]

N. Sharygina, S. Chaki, J. Ivers, and K.Wallnau. The ComFoRT reasoning framework. In Computer Aided Verification (CAV), volume 3576 of LNCS. Springer, 2005.

[SG97]

S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In O. Grumberg, editor, Proc. 9th International Conference on Computer Aided Verification (CAV’97), volume 1254, pages 72–83. Springer Verlag, 1997.

[SHADOWS]

EU STREP Project Shadows (Self-Healing Approach to Designing Complex Software Systems) https://sysrun.haifa.il.ibm.com/shadows/

[SJM2008]

M.Siuko, J.Järvenpää, J. Mattila, C. Damiani, J. Palmer. DTP2 – Verifying the Divertor Remote Handling Equipment for ITER, 22nd IAEA Fusion Energy Conference, 2008

[TK01]

Serdar Tasiran, Kurt Keutzer: Coverage Metrics for Functional Validation of Hardware Designs. IEEE Design & Test of Computers 18(4): 36-45 (2001).

[TS05]

Nikolai Tillmann and Wolfram Schulte.  Parameterized unit tests.  In  Proceedings of the 10th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2005, pages 253--262. ACM, 2005.

[UY99]

Shmuel Ur, Yoav Yadin: Micro Architecture Coverage Directed Generation of Test Programs. DAC 1999: 175-180

[UYW06]

Shmuel Ur, Elad Yom-Tov, Paul Wernick. An Open Source Simulation Model of Software Testing, Haifa Verification Conference, 2006.

[Xie05]

T. Xie and D. Notkin, Checking inside the black box: regression testing by comparing value spectra, IEEE Transactions on Software Engineering, 31(10), 869-883, 2005.

[Yang06]

J. Yang, D. Evans, D. Bhardwaj, T. Bhat and M. Das, Perracotta: mining temporal API rules from imperfect traces, in Proceeding of the 28th international conference on Software Engineering, ACM Press, 2006.



Project Publications

 

Alastair F. Donaldson, Leopold Haller, Daniel Kroening, and Philipp Rummer. "Software Verification Using k-Induction". Proceedings of SAS, 2012.

 

Leonardo Mariani and Fabrizio Pastore. "Supporting Plug-in Mashes to Ease Tool Integration". proceedings of the First International Workshop on Developing Tools as Plug-ins (TOPI) - colocated with the International Conference on Software Engineering (ICSE), 2011

 

Mauro Baluda, Pietro Braione, Giovanni Denaro, and Mauro Pezzè. "Enhancing Structural Software Coverage by Incrementally Computing Branch Executability", Software Quality Journal.

 

Dr. Hana Chockler, Alexander Ivrii, Arie Matsliah, Shiri Moran, and Ziv Nevo. "Incremental Formal Verification of Hardware". Submitted to FMCAD 2011.

[ACCEPTED]

L. Mariani and F. Pastore, "Supporting Plug-in Mashes to Ease Tool Integration", Proceedings of the 1st Workshop on Developing Tools as Plug-ins (TOPI), collocated with the International Conference on Software Engineering (ICSE), 2011.

[SUBMITTED]

D. Lo, L. Mariani and M. Santoro, "Learning Extended FSA from Software: An Empirical Assessment", International Conference on Software Testing and Analysis (ISSTA), 2011.



PINCETTE Partners Publications
ABB

 

Biallas, S., Brauer, J., Kowalewski, S., & Schlich, B. (2011). Automatically Deriving Symbolic Invariants for PLC Programs Written in IL. Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT 2010), Brunswick, Germany (pp. 237-245). Springer. Retrieved from http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bbks10.pdf.

 

Biallas, S., Kowalewski, S., & Schlich, B. (2011). Efficient Verification of Industrial PLC-Programs using Model Checking and Static Analysis. AUTOMATION 2011, Baden-Baden, Germany.

 

Brauer, J., Noll, T., & Schlich, B. (2010). Interval Analysis of Microcontroller Code using Abstract Interpretation of Hardware and Software. Software and Compilers for Embedded Systems (SCOPES 2010), St. Goar, Germany. ACM Press. doi: 10.1145/1811212.1811216.

 

Gückel, D., Schlich, B., Brauer, J., & Kowalewski, S. (2010). Synthesizing Simulators for Model Checking Microcontroller Binary Code. Design and Diagnostics of Electronic Circuits and Systems (DDECS 2010), Vienna, Austria (pp. 313-316). IEEE Computer Society Press. doi: 10.1109/DDECS.2010.5491761.

 

Reinbacher, T., Horauer, M., Schlich, B., Brauer, J., & Scheuer, F. (2011). Model Checking Embedded Software of an Industrial Knitting Machine. Int. J. Information Technology, Communication and Convergence, 1(2), 186-205. InderScience.

 

Schlich, B. (2010). Model Checking of Software for Microcontrollers. ACM Transactions on Embedded Computing Systems (TECS), 9(4), 1-27. ACM. doi: http://doi.acm.org/10.1145/1721695.1721702.

 

Schlich, B., Brauer, J., & Kowalewski, S. (2011). Application of Static Analyses for State Space Reduction to Microcontroller Binary Code. Science of Computer Programming: Special Issue on FMICS 2007 & 2008, 76(2), 100-118. Elsevier. doi: 10.1016/j.scico.2010.03.006.

 

Schlich, B., Noll, T., Brauer, J., & Brutschy, L. (2011). Reduction of Interrupt Handler Executions for Model Checking Embedded Software. Haifa Verification Conference (HVC 2009), Haifa, Israel (Vol. 6405, pp. 5-20). Springer. doi: 10.1007/978-3-642-19237-1.

 

Michael Wahler, Stefan Richter, Sumit Kumar, and Manuel Oriol. Non-disruptive Large-scale Component Updates for Real-Time Controllers. Third Workshop on Hot Topics in Software Upgrades (HotSWUp'11), 2011.

UniMiB

 

Leonardo Mariani, Fabrizio Pastore, and Mauro Pezzè. Dynamic Analysis for Diagnosing Integration Faults. IEEE Transactions on Software Engineering, 2011 (to appear; pre-print available).

 

Leonardo Mariani, Fabrizio Pastore, M. Pezzè and M. Santoro. Mining Finite-State Automata with Annotations. CRC Press, book chapter in Mining Software Specifications: Methodologies and Applications, 2011.

 

Michael W. Whalen, Patrice Godefroid, Leonardo Mariani, Andrea Polini , Nikolai Tillmann and Willem Visser. FITE: Future Integrated Testing Environment. ACM, proceedings of the Workshop on the Future of Software Engineering Research – collocated with ESEC/FSE, 2010.

 

Mauro Baluda, Pietro Braione, Giovanni Denaro, and Mauro Pezzè, Structural Coverage of Feasible Code. proceedings of the International Workshop on Automated software testing (AST) ) - colocated with the International Conference on Software Engineering (ICSE), 2010.

 

Leonardo Mariani and Fabrizio Pastore and Mauro Pezzè. A Toolset for Automated Failure Analysis. proceedings of the International Conference on Software Engineering (ICSE) - formal tool Demo, 2009.

 

Anton Babenko, Leonardo Mariani and Fabrizio Pastore. AVA: Automated Interpretation of Dynamically Detected Anomalies. ACM, proceedings of the International Symposium on Software Testing and Analysis (ISSTA), 2009.

 

David Lo, Leonardo Mariani and Mauro Pezzè. Automatic Steering of Behavioral Model Inference. proceedings of the 7th joint meeting of the European Software Engineering Conference (ESEC) and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), 2009.

 

Davide Lorenzoli, Leonardo Mariani and Mauro Pezzè. Automatic Generation of Software Behavioral Models. IEEE Computer Society, 30th International Conference on Software Engineering (ICSE), 2008.

 

Leonardo Mariani and Fabrizio Pastore. Automated Identification of Failure Causes in System Logs (ISSRE). IEEE Computer Society, proceedings of the International Symposium on Software Reliability Engineering, 2008.

USI

 

Tsitovich, A.; Sharygina, N.; Wintersteiger, C.M.; Kroening, D., Loop Summarization and Termination Analysis. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Saarbrücken, Germany, Springer (2011).

 

Bruttomesso, R.; Pek, E.; Sharygina, N., A Flexible Schema for Generating Explanations in Lazy Theory Propagation. International Conference on Formal Methods and Models for Codesign (MEMOCODE), Grenoble, France, IEEE Computer Society (2010).

 

Sharygina, N.; Tonetta, S.; Tsitovich, A., An abstraction refinement approach combining precise and approximated techniques. International Journal on Software Tools for Technology Transfer (STTT), p.1-14, Springer (2011).

Oxford

 

Angelo Brillout, Daniel Kroening, Philipp Rummer, and Thomas Wahl . Beyond Quantifier Free Interpolation in Extensions of Presburger Arithmetic. In Proceedings of VMCAI 2011, p. 88-102.

 

Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs. In the Proceedings of Computer-Aided Verification (CAV) 2011 (to appear).

 

Daniel Kroening, Joel Ouaknine, Ofer Strichman, Thomas Wahl, and James Worrell. Linear Completeness Thresholds for Bounded Model Checking. In the Proceedings of Computer-Aided Verification (CAV) 2011 (to appear).