Recent Published Papers
Here you will find some research papers and magazine and industry articles published by KindSoftware members.
- Marie Fasie, Anne Haxthausen, and Joseph Kiniry. A Rigorous Methodology for Analyzing and Designing Plug-Ins at the Third International Workshop on Developing Tools as Plug-ins
- Joseph Kiniry, Daniel Zimmerman, and Ralph Hyland. Testing Library Specifications by Verifying Conformance Tests at the International Conference on Testing and Proofs (TAP) 2012.
- Daniel Zimmerman, Joseph Kiniry, and Fintan Fairmichael. Toward Instant Gradeification at the 24th IEEE-CS Conference on Software Engineering Education and Training (CSEE&T) 2011.
- Joseph Kiniry and Daniel Zimmerman. Verified Gaming at the 1st Games and Software Engineering Workshop (GAS) 2011.
- Fintan Fairmichael and Joseph R. Kiniry. Verified Visualisation of Textual Modelling Languages at the Workshop on OCL and Textual Modelling. MODELS'10, Oslo, Norway. Our mechanical formalization in PVS is found in the Mechanized Theory section of this website. This paper has been subsequently published in revised form to the Electronic Communications of the EASST (a peer-reviewed open access journal).
- Vieri del Bianco, Dragan Stosic, and Joseph Kiniry. Agile Formality: A "Mole" of Software Engineering Practices. Agile Methods + Formal Methods (AM+FM'10).
- Dermot Cochran and Joseph Kiniry. Votail: A Formally Specified and Verified Ballot Counting System for Irish PR-STV Elections. FoVeOOS'10.
- Mikoláš Janota, Goetz Botterweck, Radu Grigore, and Joao Marques-Silva. How to Complete an Interactive Configuration Process? International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM'10).
- Radu Grigore, Julien Charles, Fintan Fairmichael, and Joseph R. Kiniry. Strongest Postcondition of Unstructured Programs. Workshop on Formal Techniques for Java Programs (FTfJP'09).
- Mikoláš Janota, Joseph R. Kiniry, and Goetz Botterweck. Formal Methods in Software Product Lines: Concepts, Survey, and Guidelines. Lero Technical Report Lero-TR-SPL-2008-02, University of Limerick, May 2008.
- Joseph Kiniry and Daniel Zimmerman. A Verification-centric Software Development Process for Java. The 9th International Conference on Software Quality (QSIC'09). Jeju, Korea. August, 2009.
- Joseph R. Kiniry and Fintan Fairmichael. Ensuring Consistency between Designs, Documentation, Formal Specifications, and Implementations. The 12th International Symposium on Component Based Software Engineering (CBSE'09), East Stroudsburg University, Pennsylvania, USA.
- Mikoláš Janota, Fintan Fairmichael, Viliam Holub, Radu Grigore, Julien Charles, Dermot Cochran, and Joseph Kiniry. CLOPS: A DSL for Command Line Options. IFIP Working Conference on Domain Specific Languages (DSL WC), Oxford, 2009.
- Mikoláš Janota, Victoria Kuzina, and Andrzej Wasowski. Model Construction with External Constraints: An Interactive Journey from Semantics to Syntax. 11th International Conference on Model Driven Engineering Languages and Systems Fundamental Approaches to Software Engineering (MODELS'08). Toulouse, France. September, 2008.
- Mikoláš Janota. Do SAT Solvers Make Good Configurators?. First Workshop on Analyses of Software Product Lines (ASPL'08). Limerick, Ireland, September 12, 2008.
- Julien Charles and Joseph Kiniry. A Lightweight Theorem Prover Interface for Eclipse. User Interfaces for Theorem Proving (UITP'08). A subsequent version was published in ENTCS.
- Joseph Kiniry and Daniel Zimmerman. Secret Ninja Formal Methods. The 15th International Symposium on Formal Methods (FM'08). Turku, Finland. May, 2008.
- Mikoláš Janota and Goetz Botterweck. Formal Approach to Integrating Feature and Architecture Models. Fundamental Approaches to Software Engineering (FASE'08). Budapest, Hungary. April, 2008.
- Radu Grigore and Michał Moskal. Edit and Verify. The 6th International Workshop on First-Order Theorem Proving (FTP'07). Liverpool, United Kingdom. September, 2007.
- Mikoláš Janota, Radu Grigore, and Michał Moskal. Reachability Analysis for Annotated Code. The 6th International Workshop on the Specification and Verification of Component-based Systems (SAVCBS'07). Dubrovnik, Croatia. September, 2007.
Mikoláš Janota and
Reasoning about Feature Models in Higher-Order Logic.
The 11th International Software Product Lines Conference
Kyoto, Japan. September, 2007.
Our mechanical formalization in PVS is found in the Mechanized Theory section of this website.
- Joseph Kiniry, Dermot Cochran, and Patrick Tierney. A Verification-Centric Realization of e-Voting. The USENIX/ACCURATE Electronic Voting Technologies Workshop (EVT'07). Boston, Massachusetts. August, 2007.
- Michał Moskal, Jakub Łopuszański, and Joseph Kiniry. E-matching for Fun and Profit. The 5th International Workshop on Satisfiability Modulo Theories (SMT'07). Berlin, Germany. July, 2007.
- Joseph Kiniry. Formally Counting Electronic Votes (But Still Only Trusting Paper). The 12 International Conference on Engineering of Complex Computing Systems (ICECCS'07). Auckland, New Zealand. July, 2007.
- Mikoláš Janota, Assertion-based Loop Invariant Generation. The 1st International Workshop on Invariant Generation (WING'07). Hagenberg, Austria. June, 2007.
- Joseph Kiniry, Alan Morkan, Dermot Cochran, Fintan Fairmichael, Patrice Chalin, Martijn Oostdijk, and Engelbert Hubbers. The KOA Remote Voting System: A Summary of Work To Date. The 2nd International Symposium on Trustworthy Global Computing (TGC'06). Lucca, Italy. November, 2006.
- Joseph Kiniry, Alan Morkan, and Barry Denby. Soundness and Completeness Warnings in ESC/Java2. The 5th International Workshop on the Specification and Verification of Component-based Software (SAVCBS'06). Portland, Oregon. November, 2006.
- Joseph Kiniry. Exceptions in Java and Eiffel: Two Extremes in Exception Design and Application. In C. Dony et al. (Eds.): Exception Handling, LNCS 4119, pp. 288-300, 2006.
- Patrice Chalin, Joseph Kiniry, Gary T. Leavens, and Erik Poll. Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2. The 4th International Symposium on Formal Methods for Components and Objects (FMCO'05). Amsterdam, The Netherlands. November, 2006.
- Patrice Chalin, Clément Hurlin, and Joseph Kiniry. Integrating Static Checking and Interactive Verification: Supporting Multiple Theories and Provers in Verification. The 1st International Conference on Verified Software: Tools, Technologies, and Experiences (VSTTE'05). Zurich, Switzerland. October, 2005.