(Preprints are provided for personal use only. Please respect the respective publisher's copyright and use publisher's version where possible.)
Temporal Logic Synthesis |
|
| [BCG+10] | R. Bloem, A. Cimatti, K. Greimel, G. Hofferek, R. Könighofer, M. Roveri, V. Schuppan, R. Seeber: RATSY - A new Requirements Analysis Tool with Synthesis. In: B. Cook, P. Jackson, T. Touili (eds.): Proceedings of the 22nd International Conference on Computer Aided Verification (CAV'10), Edinburgh, UK, July 15-19, 2010. To appear. Lecture Notes in Computer Science. Springer, 2010. Download: preprint (zipped) |
| [CRST08] | A. Cimatti, M. Roveri, V. Schuppan, A. Tchaltsev: Diagnostic Information for Realizability. In: F. Logozzo, D. Peled, L. Zuck (eds.): Proceedings of the 9th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'08), San Francisco, CA, USA, January 7-9, 2008. Volume 4905 of Lecture Notes in Computer Science, pp. 52-67. Springer, 2008. Acceptance rate: 21 out of over 60 (< 35 %). Download: publisher, preprint (zipped), BibTeX, experiments |
Temporal Logic Satisfiability |
|
| [Sch10a] | V. Schuppan: Towards a Notion of Unsatisfiable Cores for LTL. In: F. Arbab, M. Sirjani (eds.): Fundamentals of Software Engineering, Third IPM International Conference, FSEN 2009, Kish Island, Iran, April 15-17, 2009, Revised Selected Papers. Volume 5961 of Lecture Notes in Computer Science, pp. 129-145. Springer, 2010. For the full version see [Sch09b], for the pre-proceedings version see [Sch09a]. Download: publisher, local (zipped), BibTeX |
| [Sch09a] | V. Schuppan: Towards a Notion of Unsatisfiable Cores for LTL. In: F. Arbab, M. Sirjani (eds.): Pre-Proceedings of the 3rd International Conference on Fundamentals of Software Engineering (FSEN'09), Kish Island, Persian Gulf, Iran, April 15-17, 2009, pp. 57-72. Acceptance rate: 22 regular papers (+ 5 short papers and 7 poster presentations) out of 88 submissions (25 %). Best Paper Award. For the full version see [Sch09b], for the post-proceedings version see [Sch10a]. Download: preprint (zipped), BibTeX, slides |
| [Sch09b] | V. Schuppan: Towards a Notion of Unsatisfiable Cores for LTL. Technical Report 200901000, Fondazione Bruno Kessler, 2009. Full version of [Sch09a], [Sch10a]. Download: preprint (zipped), BibTeX |
| [CRST07] | A. Cimatti, M. Roveri, V. Schuppan, S. Tonetta: Boolean Abstraction for Temporal Logic Satisfiability. In: W. Damm, H. Hermanns (eds.): Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07), Berlin, Germany, July 3-7, 2007. Volume 4590 of Lecture Notes in Computer Science, pp. 532-546. Springer, 2007. Acceptance rate: 33 out of 134 (25 %). Download: publisher, preprint (zipped), extended version (zipped), BibTeX, slides, experiments and full set of plots |
Model Checking |
|
| [ESB+09] | S. Edelkamp, V. Schuppan, D. Bosnacki, A. Wijs, A. Fehnker, H. Aljazzar: Survey on Directed Model Checking. Invited contribution (not peer-reviewed). In: D. Peled, M. Wooldridge (eds.): 5th International Workshop on Model Checking and Artificial Intelligence (MoChArt'08), Revised Selected and Invited Papers, Patras, Greece, July 21, 2008. Volume 5348 of Lecture Notes in Computer Science, pp. 65--89. Springer, 2009. Download: publisher, preprint (zipped), BibTeX |
| [BHJ+06] | A. Biere, K. Heljanko, T. Junttila, T. Latvala, V. Schuppan: Linear Encodings of Bounded LTL Model Checking. In: K. Etessami, S. Rajamani (eds.): Selected Papers of the Conference "Computer Aided Verification 2005", Logical Methods in Computer Science 2 (5:5) 2006. Download: publisher, preprint (zipped), BibTeX |
| [SB05a] | V. Schuppan, A. Biere: Shortest Counterexamples for Symbolic Model Checking of LTL with Past. In: N. Halbwachs, L. Zuck (eds.): Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05), Edinburgh, UK, April 4-8, 2005. Volume 3440 of Lecture Notes in Computer Science, pp. 493-509. Springer, 2005. Acceptance rate: 33 out of 141 (23 %). For the full version see [SB05c]. Download: publisher, preprint (zipped), BibTeX, slides, SMV models |
| [SB05b] | V. Schuppan, A. Biere: Liveness Checking as Safety Checking for Infinite State Spaces. In: S. Smolka and J. Srba (eds.): Proceedings of the 7th International Workshop on Verification of Infinite-State Systems (INFINITY'05), San Francisco, CA, USA, August 27, 2005. Electronic Notes in Theoretical Computer Science 149 (1), pp. 79-96. Elsevier, 2006. Full version of [SB05d]. Download: publisher, preprint (zipped), BibTeX |
| [SB05c] | V. Schuppan, A. Biere: Shortest Counterexamples for Symbolic Model Checking of LTL with Past. Technical Reports 470, ETH Zürich, Department of Computer Science, 01/2005. Full version of [SB05a]. Download: publisher, preprint (zipped), BibTeX |
| [SB05d] | V. Schuppan, A. Biere: Liveness Checking as Safety Checking for Infinite State Spaces. In: S. Smolka and J. Srba (eds.): Preliminary Proceedings of the 7th International Workshop on Verification of Infinite-State Systems (INFINITY'05), San Francisco, CA, USA, August 27, 2005, pp. 53-64. For the full version see [SB05b]. Download: publisher, preprint (zipped), BibTeX, slides |
| [SB04] | V. Schuppan, A. Biere: Efficient reduction of finite state model checking to reachability analysis. In: International Journal on Software Tools for Technology Transfer (STTT) (2004) 5: pp. 185-204. Substantially extended and corrected version of [BAS02]. Download: publisher, preprint (zipped), BibTeX, SMV models |
| [BAS02] | A. Biere, C. Artho, V. Schuppan: Liveness Checking as Safety Checking. In: R. Cleaveland, H. Garavel (eds.): Proceedings of the Seventh International Workshop on Formal Methods for Industrial Critical Systems (FMICS'02), Malaga, Spain, July 12-13, 2002. Acceptance rate: 13 out of 22 (59 %). For a substantially extended and corrected version see [SB04]. Download: publisher, preprint (zipped), BibTeX, slides |
Java Checking |
|
| [ABH+06] | C. Artho, A. Biere, S. Honiden, V. Schuppan, P. Eugster, M. Baur, B. Zweimüller, P. Farkas: Advanced Unit Testing - How to Scale Up a Unit Test Framework. In: Proceedings of the 1st International Workshop on Automation of Software Test (AST'06), Shanghai, China, May 23, 2006, pp. 92-98. ACM Press, 2006. Download: publisher, preprint (zipped), BibTeX |
| [ASB+04] | C. Artho, V. Schuppan, A. Biere, P. Eugster, M. Baur, B. Zweimüller: JNuke: Efficient Dynamic Analysis for Java. In: R. Alur, D. Peled (eds.): Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04), Boston, MA, USA, July 13-17, 2004. Volume 3114 of Lecture Notes in Computer Science, pp. 462-465. Springer, 2004. Download: publisher, preprint (zipped), BibTeX |
| [SBB04] | V. Schuppan, M. Baur, A. Biere: JVM Independent Replay in Java. In: K. Havelund, G. Rosu (eds.): Proceedings of the Fourth Workshop on Runtime Verification (RV'04), Barcelona, Spain, April 3-4, 2004. Volume 113 of Electronic Notes in Theoretical Computer Science, pp. 85-104. Elsevier, 2005. Acceptance rate: 11 out of 13 (85 %). Download: publisher, preprint (zipped), BibTeX, slides |
Case Study: IEEE 1394 FireWire |
|
| [SB03] | V. Schuppan, A. Biere: Verifying the IEEE 1394 FireWire Tree Identify Protocol with SMV. In: Formal Aspects of Computing (2003) 14: pp. 267-280. Extended version of [SB01]. Download: publisher, preprint (zipped), BibTeX, SMV models |
| [SB01] | V. Schuppan, A. Biere: A Simple Verification of the Tree Identify Protocol with SMV. In: S. Maharaj, J. Romijn, C. Shankland (eds.): Proceedings of the IEEE 1394 (FireWire) Workshop, pp. 31-34, Berlin, Germany, March 13, 2001. Department of Computing Science and Mathematics, University of Stirling, March 2001. For an extended version see [SB03]. Download: full text (zipped), BibTeX, slides |
Evaluating V-Model 97 with CMM |
|
| [SR00] | V. Schuppan, W. Rußwurm: A CMM-Based Evaluation of the V-Model 97. In: R. Conradi (ed.), Proceedings of the 7th European Workshop on Software Process Technology (EWSPT'00), Kaprun, Austria, February 21-25, 2000. Volume 1780 of Lecture Notes in Computer Science, pp. 69-83. Springer, 2000. Acceptance rate: 21 out of 44 (48 %). Download: publisher, preprint (zipped), BibTeX |
| [SR99] | V. Schuppan, W. Rußwurm: Das V-Modell 97 auf dem Weg zum CMM-konformen Standard (The V-Model 97 aiming to become CMM-compliant standard). In: Software@Siemens, December 1999: pp. 40-42. Siemens AG, 1999. Download: scan (zipped), BibTeX. A shorter version also appeared in the English edition: Software@Siemens, February 2000: pp. 54-55. Siemens AG, 2000. Download: scan (zipped), BibTeX |
Theses |
|
| [Sch06] | V. Schuppan: Liveness Checking as Safety Checking to Find Shortest Counterexamples to Linear Time Properties (Ph.D. thesis). Diss. ETH No. 16268, Swiss Federal Institute of Technology, 2006. Published by Verlag Dr. Hut, Munich, Germany, ISBN 3-89963-337-7, 2006. Download: ETH E-Collection, PDF (zipped), BibTeX, slides (defense) |
| [Sch99] | V. Schuppan: Das V-Modell 97 als Softwareentwicklungsprozeß aus der Sicht des Capability Maturity Models (CMM) für Software (Master's thesis). Diplomarbeit, Institut für Informatik, Technische Universität München, 1999. Download: full text (zipped), BibTeX |
Other |
|
| [Sch97] | V. Schuppan: Verschlüsselungsfreiheit soll eingeschränkt werden (Encryption to be controlled). In: impulsiv, Nr. 57, May 1997: p. 7. Fachschaft Math/Phys/Info. (Student magazine for maths/physics/CS students at TU München). Download: publisher, scan (zipped). A shorter version also appeared in: PANIK, Ausgabe 23, June 1997: p. 21. Studentische Vertretung der TU München. (Student magazine for all students at TU München). Download: scan (zipped) |
|
© Viktor Schuppan Last Modified 13 June 2010 |