Joseph Kiniry

Biography

Research Interests:

• (end-to-end) electronic voting systems
• Applied formal methods
• distributed systems
• foundations of mathematics
• functional
• object-oriented and component-based systems and languages
• software engineering
• software/system/network security

General

Name and Title: 

Joseph Kiniry

Email: 

From January 2010 onward Joseph Kiniry is an Associate Professor at the IT University of Copenhagen (ITU).

http://www1.itu.dk/

• Biography
• Professional
• Publications
• Research
• Teaching
• Collaborators

Biography

I am a lecturer (what would be called an assistant professor with tenure elsewhere in the world) in the School of Computer Science and Informatics at University College Dublin (aka UCD, and sometimes known as the National University of Ireland, Dublin). I help lead the Systems Research Group (SRG).

From January 2010 I will be an Associate Professor at the IT University of Copenhagen (ITU).  I will be working in the Software Development Group (SDG) and with the Programming, Logic, and Semantics (PLS) group.

My KindSoftware research group is partially funded by the European Project Mobius within the IST 6th Framework and CHARTER within the IST 7th Framework, by the Science Foundation Ireland via the UCD CASL SenseTile grant and the Lero: The Irish Software Engineering Research Centre, the EU Framework Program via the  COST Program (European Cooperation in the field of Scientific and Technical Research) action IC0701 "Formal Verification of Object-Oriented Software," the IRCSET Embark Initiative, and UCD. My total funding since 2005 is approximately 1.5M Euro.

Between October 2002 and October/November 2004, I was a postdoctoral scholar in the Security of Systems (SoS) Group in the Nijmegen Institute for Computing and Information Science at the Radboud University Nijmegen.

I am a Ph.D. graduate of the Department of Computer Science at the California Institute of Technology. I am also an entrepreneur. I have started five companies thus far and I am an independent consultant with well over a decade of experience.

I am interested in formal methods, foundations of mathematics, software engineering, software/system/network security, distributed systems, object-oriented and component-based systems and languages, (end-to-end) electronic voting systems, knowledge representation, systems modeling, artificial life, and the many different theoretical underpinnings of computing. In short, I am a Computer Scientist/Mathematician researcher and hacker, in the old sense of the term.

See the KindSoftware website for updates about my work.

Professional

Professional Associations:

• Association: ACM, Function/Role: Professional Member
• Association: IEEE, Function/Role: Professional Member
• Association: IEEE Computer Society, Function/Role: Professional Member
• Association: AMS, Function/Role: Professional Member
• Association: MAA, Function/Role: Professional Member
• Association: AAAS, Function/Role: Professional Member
• Association: USENIX, Function/Role: Professional Member

Patents:

• Patent 6,898,791 : Infospheres Distributed Object System (a precursor to Sun's Jini and ObjectSpace's Voyager)

Conference Contributions:

• Kiniry, J. (2008) Talk title: Verified Gaming. [Invited Lecture], GC6 Workshop on "Pilot Projects for the Grand Challenge in Verified Software", Turku, Finland , 27-MAY-08 - 27-MAY-08.
• Woodcock, J. and Hoare, C.A.R. and Kiniry, J. (2008) Talk title: Program Verification for the Masses. [Invited Lecture], British Computer Society (BCS) GC6 Town Hall meeting, London , 04-FEB-08 - 04-FEB-08.
• Kiniry, J. (2007) Talk title: Formally Counting Electronic Votes (But Still Only Trusting Paper). [Keynote Address], The 12th International Conference on Engineering of Complex Computer Systems (ICECCS), Auckland, New Zealand , 11-JUL-07 - 14-JUL-07.
• Kiniry, J. (2007) Talk title: Recent Advances in Extended Static Checking. [Keynote Address], 6th International KeY Symposium, Westerwald (near Koblenz), Germany , 14-JUN-07 - 16-JUN-07.
• Kiniry, J. (2006) Talk title: Program Safety via Programmer Safety. [Keynote Address], The 2nd International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA), Cyprus , 15-SEP-06 - 19-SEP-06.
• Kiniry, J. (2006) Talk title: (Deeply) Integrating Proving and Programming. [Keynote Address], Automated Formal Methods 2006, Seattle , 21-AUG-06 - 21-AUG-06.
• Kiniry, J. (2005) Talk title: Integrating Static Checking and Interactive Verification: Supporting Multiple Theories and Provers in Verification. [Invited Lecture], The 1st International Conference on Verified Software, Tools, Technology, and Experiences (VSTTE, Zurich , 10-OCT-05 - 14-OCT-05.

Committee Work:

• Committee : PhD committee, Joachim van dem Berg
• Committee : RE-VOTE 2009. Member of Program Committee.
• Committee : VSTTE 2010. Member of Program Committee.
• Committee : SLE 2008. Member of Program Committee.
• Committee : COST Program Action IC0701
• Committee : PhD committee, Thomas Wilson, Stirling University
• Committee : PhD committee, Humayun Kabir, Dublin City University
• Committee : PhD committee, Georg Jung, Kansas State University
• Committee : PhD committee, Mircea Trofin, University College Dublin
• Committee : PhD committee, Martijn Warnier, Radboud University Nijmegen
• Committee : PhD committee, Cees-Bart Breunesse, Radboud University Nijmegen
• Committee : VAMP 2009 Program Committee
• Committee : VERIFY 2008. Member of Program Committee.
• Committee : WOTE 2008. Member of Program Committee.
• Committee : ICTAC 2008. Member of Program Committee.
• Committee : CBSE 2008. Member of Program Committee.
• Committee : OSS 2008. Member of Program Committee.
• Committee : Member of JML Consortium.
• Committee : IFM 2008. Member of Program Committee.
• Committee : TOOLS 2008. Member of Program Committee.
• Committee : SAS II 2007. Member of Program Committee.
• Committee : Member of the Governing Board of the Grand Challenge 6: Verified Software Repository project.
• Committee : SEFM 2007. Member of Program Committee.
• Committee : VERIFY 2007. Member of Program Committee.
• Committee : VAMP 2007. Member of Program Committee and Organizer.
• Committee : TOPMoDelS 2007. Member of Program Committee.
• Committee : OSS 2007. Member of Program Committee.
• Committee : ICTAC 2007. Member of Program Committee.
• Committee : TOOLS 2007. Member of Program Committee.
• Committee : ISoLA 2006. Member of Program Committee.
• Committee : IFL 2005. Member of Program Committee.
• Committee : FTfJP 2005. Member of Program Committee.
• Committee : FTfJP 2004. Member of Program Committee.
• Committee : SAVCBS 2005. Member of Program Committee.
• Committee : SAVCBS 2006. Member of Program Committee.
• Committee : OOPSLA 2001. Member of Program Committee.

Employment:

• Employer: Radboud University Nijmegen
  Position: Postdoctoral Scholar
• Employer: California Institute of Technology
  Position: PhD Student, Research Assistant, Teaching Assistant
• Employer: DALi, Inc.
  Position: Co-founder and Chief Scientist

Education:

• Year 2002 Institution: California Institute of Technology
  Qualification: PhD Subject:
• Year 1998 Institution: California Institute of Technology
  Qualification: MSc Subject:
• Year 1995 Institution: Uni of Massachusetts, Amherst
  Qualification: MSc Subject:
• Year 1992 Institution: Florida State Univ. FL. USA
  Qualification: BS Subject:
• Year 1992 Institution: Florida State Univ. FL. USA
  Qualification: BSc Subject:

Languages:

• English:
• French:
• Spanish:
• Dutch:
• German:

Consultancy:

• Client: : Ireland Revenue

Other:

• The Java Modeling Language (JML) 

  Another major research output over the past few years includes my work on the Java Modeling Language (JML).
  
  This work is summarized in the journal paper: "An Overview of JML Tools and Applications", with Lilian Burdy, Yoonsik Cheon, David Cok, Michael Ernst, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. International Journal on Software Tools for Technology Transfer, February, 2005, which has several dozen citations.
  
  This journal paper summarizes many years of work on the JML specification language, and the major tools supporting JML, by several research groups. My group here at UCD is one of the leaders of the JML effort, which is now supported by a major NSF Infrastructure grant in the U.S.A. (on which I am an external investigator/supporter) and a small FME grant (on which I am the P.I.) here in Europe.
  
  I have also given half a dozen well-attended and reviewed tutorials on JML and related tools at several major international conferences (e.g., ETAPS, ECOOP, FM, ESEC/FSE, FMCO, etc.) over the past four years, and am continuing to give new ones now (I am scheduled for ETAPS 2008 and 2009 at this moment, e.g.).
  
  I have also co-written several booklets on JML and JML-related tools, totally several hundred pages of documentation. The titles of these documents are "The Java Modeling Language Reference Manual", "The ESC/Java2 Reference Manual", "Extending ESC/Java2", "The Logics and Calculi of ESC/Java2", "The Provers of ESC/Java2", and "ESC/Java2 Implementation Notes".
  
  A selection of other research papers directly supporting this work include:
  
  - Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2, with
  Patrice Chalin, Gary T. Leavens, and Erik Poll. Proceedings of Formal Methods for Components and Object (FMCO) 2005. Amsterdam, The Netherlands, 2006.
  – Integrating Static Checking and Interactive Verification: Supporting Multiple Theories and Provers in Verification, with Patrice Chalin and Clement Hurlin. Proceedings of Verified Software: Tools, Technologies, and Experiences (VSTTE) 2005. Zurich, Switzerland, 2005.
  - ESC/Java2: Uniting ESC/Java and JML: Progress and issues in building and using ESC/Java2 and a report on a case study involving the use of ESC/Java2 to verify portions of an Internet voting tally system, with David Cok. Proceedings of the International Workshop on the Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS) 2004. Marseille, France, March, 2004.
  - Soundness and Completeness Warnings in ESC/Java2, with Alan Morkan and Barry Denby.
  Proceedings of Specification and Verification of Component-based Software (SAVCBS) 2006.
  Portland, Oregon, 2006.

• Designing, Constructing, Shipping, and Supporting Several
  Complex, Popular, and Well-known
  Applied Formal Methods Software Systems 

  Another major research output over the past few years includes my work on designing, constructing, shipping, and supporting nearly twenty shipped versions of eight major pieces of software: BONc, ESC/Java2, IDebug, Javafe, KOA, Mobius, OBJ3, and Simplify.

   

• Electronic/Computer-based Voting Research, Consulting, and Activism 

  Another major research output over the past few years includes my scientific, government consulting, and activist work on e-voting in Ireland, The Netherlands, and the U.S.A.

• Program Committee Memberships I have been invited to sit on the PC of nearly twenty top conferences and a handful of workshops over the past three years. 

• Governing Board Memberships

  I have been asked to sit two boards of major scientific efforts:

  • the Governing Board of the Grand Challenge 6: Verified Software Repository project, and http://www.fmnet.info/gc6/
    http://www.fmnet.info/vsr-net/
  • the JML Consortium (the body relating to the aforementioned NSF grant).  http://www.jmlspecs.org/

• Keynote Speaker

  I have been a keynote speaker at nine top international conferences and related events over the past three years including:

  • The British Computer Society (BCS) GC6 Town Hall meeting in London in February, 2008;
  • The 12th International Conference on Engineering of Complex Computer Systems (ICECCS) in New Zealand in July, 2007;
  • The 6th International KeY Symposium in Germany in June, 2007;
  • The 2nd International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA) in Cyprus in 2006;
  • Automated Formal Methods (AFM) at the Federated Logic Conference (FLoC) in Seattle in 2006;
  • Invited to, and gave talks and sat on panels at, three Dagstuhl workshops on verification and e-voting (2006-2007); and
  • The 1st International Conference on Verified Software, Tools, Technology, and Experiences (VSTTE) in Zurich in 2005.

Publications

Books:

• Desmond D'Souza and Alan Wills (1998) Object, Components, and Frameworks - The Catalysis Approach (primary technical reviewer). *: Addison-Wesley. [Details]

Peer Reviewed Journals:

• Moskal, M. and Kiniry, J. and Lopuszanski, J. (2008) 'E-matching for Fun and Profit'. Electronic Notes in Theoretical Computer Science, Special Issue on SMT Solvers, . [Details]
• Chalin, P, Kiniry, JR, Leavens, GT, Poll, E, (2006) 'Beyond assertions: Advanced specification and verification with JML and ESC/Java2'. LOCATION- AND CONTEXT-AWARENESS, PROCEEDINGS, 4111 (NA):342-363. [Details]
• Lilian Burdy, Yoonsik Cheon, David Cok, Michael D. Ernst, Joe Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll (2004) 'An Overview of JML Tools and Applications'. International Journal on Software Tools for Technology Transfer, . [Details]
• Kiniry, J. (2006) 'Exceptions in Java and Eiffel: Two Extremes in Exception Design and Application'. Lecture Notes in Computer Science, 3013 . [Details]
• Kiniry, J. (2004) 'Formalizing the User's Context to Support User Interfaces for Integrated Mathematical Environments'. Electronic Notes in Theoretical Computer Science, Special Issue on User Interfaces for Theorem Proving, . [Details]
• Kiniry, J., K. Mani Chandy, Adam Rifkin, and Daniel M. Zimmerman (1997) 'Webs of Archived Distributed Computations for Asynchronous Collaboration'. Journal of Supercomputing, 11 (2). [Details]

Other Journals:

• J. Kiniry, W. Pieters (2005) 'Internet Voting Not Impossible' COMMUNICATIONS OF THE ACM . [Details]
• Kiniry, J., Vincent Pollmeier, Lena Smith, Roman Ginis, et al, (2000) 'At the Crossroads of Law and Technology: A Simulated Infringement Case Arising in Cyberspace' Loyola Law Review of Los Angeles 33 (3) . [Details]

Conference Publications:

• Kiniry, J. and Zimmerman, D. (2009) A Verification-centric Software Development Process for Java The 9th International Conference on Software Quality [Details]
• Kiniry, J. et al (2006) KOA Remote Voting System: A summary of work to date Trusted Global Computing Lucca, Italy, [Details]
• Kiniry, J. and Fairmichael, F. (2009) Ensuring Consistency between Designs, Documentation, Formal Specifications, and Implementations Component-based Software Engineering (CBSE 2009) [Details]
• Janota, M. et al. (2009) CLOPS: A DSL for Command Line Options IFIP Domain Specific Languages Working Conference (DSL-WC 2009) [Details]
• Kiniry, J. and Chandy, K.M. and Sivilotti, P. (1998) A Cottage Industry of Software Publishing: Implications for Theories of Composition Formal Methods for Parallel Programming: Theory and Applications (FMPPTA) 1998 [Details]
• Joseph Kiniry and Daniel Zimmerman (2008) Secret Ninja Formal Methods Formal Methods (FM) [Details]
• Janota, M. and Kiniry, J. (2007) Reasoning about Feature Models in Higher-Order Logic Software Product Lines (SPL) Kyoto, Japan, [Details]
• Kiniry, J. and Cochran, D. and Tierney, P. (2007) A Verification-Centric Realization of e-Voting USENIX/ACCURATE Electronic Voting Technologies (EVT) [Details]
• Michał Moskal and Jakub Łopuszański and Joseph Kiniry (2007) E-matching for Fun and Profit Satisfiability Modulo Theories (SMT) [Details]
• Joseph Kiniry (2007) Formally Counting Electronic Votes (But Still Only Trusting Paper) International Conference on Engineering of Complex Computing Systems (ICECCS) [Details]
• Morkan, A. and Cochran, D. and Fairmichael, F. and Chalin, P. and Oostdijk, M. and Hubbers, E. and Kiniry, J. (2006) The KOA Remote Voting System: A Summary of Work To Date Trustworthy Global Computing (TGC) [Details]
• Kiniry, J. and Morkan, A. and Denby, B. (2006) Soundness and Completeness Warnings in ESC/Java2 The 5th International Workshop on the Specification and Verification of Component-based Software (SAVCBS 2006) [Details]
• Kiniry, J. and Chalin, P. and Leavens, G.T. and Poll, E. (2006) Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2 Formal Methods for Components and Objects (FMCO) , pp.342-363 [Details]
• Kiniry, J. and Chalin, P. and Hurlin, C. (2006) Integrating Static Checking and Interactive Verification: Supporting Multiple Theories and Provers in Verification Verified Software: Tools, Technologies, and Experiences (VSTTE) [Details]
• Cok, D.R. and Kiniry, J. (2005) ESC/Java2: Uniting ESC/Java and JML Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS) , pp.108-128 [Details]
• Kiniry, J. and Owre, S. (2003) Improving the PVS User Interface User Interfaces for Theorem Proving (UITP) Rome, Italy, [Details]
• Jacobs, B. and Kiniry, J. and Warnier, M. (2003) Java Program Verification Challenges Formal Methods for Components and Objects (FMCO) [Details]

Other Publications:

• Grigore, R. et al. (2009) Strongest Postcondition of Unstructured Programs. Formal Techniques for Java-like Programs: Workshops [Details]
• Charles, J. and Kiniry, J. (2008) A Lightweight Theorem Prover Interface for Eclipse. User Interfaces for Theorem Proving (UITP at TPHOL'08): Workshops [Details]
• Kiniry, J., Hubbers, E., Jacobs, B., and Oostdijk, M. (2004) Counting Votes with Formal Methods. Invited papers [Details]
• Kiniry, J. (2003) Opportunities and Challenges for Formal Specification of Java Programs. Prato, Italy: Workshops [Details]
• Kiniry, J. (1998) The Specification of Dynamic Distributed Component Systems. Dissertations/Theses [Details]
• Kiniry, J. (2002) Kind Theory. Dissertations/Theses [Details]
• Kiniry, J. (1995) DECS: A Distributed Enterprising Computing System. Dissertations/Theses [Details]
• Kiniry, J. (1992) CUI3D: A 3D Interface for the CLAS Detector. Dissertations/Theses [Details]

Research

Research Interests:

I primarily perform research in applied formal methods for software engineering, semantics, distributed object and component-based computing, and system and component specification, particularly with regards to system correctness and security. I also have research interests in system modeling, programming languages, compilers, networking, operating systems, graphics, artificial life, education, and ethics.

Research Projects:

• Sponsor : Enterprise Ireland (EI)
  Title : Critical and High Assurance Requirements Transformed through Engineering Rigour (CHARTER)
  Start Date / End Date : 01-AUG-09 / 31-MAR-12
• Sponsor : Formal Methods Europe
  Title : JML Reloaded
  Start Date / End Date : 01-APR-08 / 31-MAR-10
• Sponsor : Irish Research Council for Science Engineering and Technology (IRCSET)
  Title : Formalised distributed collaborative software engineering
  Start Date / End Date : 11-SEP-06 / 11-SEP-09
• Sponsor : European Commission FP6
  Title : MOBIUS: Mobility, Ubiquity and Security
  Start Date / End Date : 01-SEP-05 / 01-SEP-09
• Sponsor : University College Dublin (UCD)
  Title : Distributed collaborative verification of concurrent software systems
  Start Date / End Date : 01-AUG-06 / 31-JUL-07
• Sponsor : Enterprise Ireland (EI)
  Title : Coordinating the verified software grand challenge
  Start Date / End Date : 01-MAY-06 / 01-MAY-07
• Sponsor : Enterprise Ireland (EI)
  Title : ESC/JAVA 2
  Start Date / End Date : 10-MAY-05 / 10-JUN-05
• Sponsor : Irish Research Council for Science Engineering and Technology (IRCSET)
  Title : Proof transforming compiler and on-device proof checking
  Start Date / End Date : 26-SEP-05 / 26-SEP-08

Teaching

Teaching Interests:

I teach computer science and mathematics.  I am a respected speaker in academic and industry settings, I've lectured to hundreds of students at all levels over the years, and I get great reviews in all my classes.  The graduate-level computer science courses that I would enjoy teaching include formal methods, software engineering, programming languages, distributed systems, operating systems, algorithms, computer graphics, simulation, and artificial life.  The graduate-level mathematics courses that I have enjoyed teaching include: logic, category theory, type theory, advanced algebra, and model theory.  I am capable of teaching nearly any undergraduate course in computer science and pure or applied mathematics.
 

Modules Co-ordinated:

• COMP30010     Computer Science: Foundations of Computing
• COMP40690     Computer Science: Dependable & Reliable Software Systems
• COMP47100     Computer Science: Dependable and Reliable Software Systems (PhD)

Current Postgraduate Students:

• Dermot Cochran, Doctor of Philosophy (PhD)   -   Thesis Supervisor
• Fintan Fairmichael, Doctor of Philosophy (PhD)   -   Thesis Supervisor
• Radu Grigore, Doctor of Philosophy (PhD)   -   Thesis Supervisor
• Mikolas Janota, Doctor of Philosophy (PhD)   -   Thesis Supervisor

Collaborators

Internal Collaborators:

• I have ongoing collaborations with the following academics at UCD: Paddy Nixon, Aaron Quigley, Simon Dobson (all School of Computer Science and Informatics), Scott Rickard (School of Electrical, Electronic and Mechanical Engineering), Chris Bean (School of Geological Sciences), Gary McGuire (School of Mathematical Sciences), and Marcus Greferath (School of Mathematical Sciences). I also, of course, collaborate with my PhD students Radu Grigore, Fintan Fairmichael, and Mikolas Janota; past PhD student Alan Morkan; my MSc students Robin Green and Alan Barrett; and my research programmer Dermot Cochran. UCD undergraduate students Jakub Dostal, Patrick Tierney, Barry Denby, Robert Finlay, Daragh Hurley, Niall O'Higgens, Conor Gallagher, and Rory McCann also collaborated with me in the past.

External Collaborators:

• I have a large number of external collaborators from all over the world. Some of my recent senior collaborators include Baptiste Alcalde (Luxembourgh), Lilian Burdy (INRIA), Patrice Chalin (Concordia), Mani Chandy (Caltech), Yoonsik Cheon (Texas), David Cok (Kodak), Michael Ernst (MIT), Roman Ginis (Caltech), Engelbert Hubbers (Nijmegen), Clément Hurlin (INRIA), Bart Jacobs (Nijmegen), Gary Leavens (UCF), Rustan Leino (Microsoft Research), Michal Moskal (Microsoft Research), Erik Poll (Nijmegen), Martijn Oostdijk (Nijmegen), Sam Owre (SRI), Adam Rifkin (Caltech), Peter Ryan (Newcastle), Paul Sivilotti (Caltech), Cesare Tinelli (Iowa), Martijn Warnier (Nijmegen), Daniel Zimmerman (Washington), and others.