Secret Ninja Formal Methods (2008)
Joseph R. Kiniry, Daniel M. Zimmerman
Abstract. The use of formal methods can significantly improve software quality. However, many instructors and students consider formal methods to be too difficult, impractical, and esoteric for use...
E-matching for Fun and Profit (2008)
Efficient handling of quantifiers is crucial for solving software verification problems. E-matching algorithms are used in satisfability modulo theories solvers that handle quantified formulas...
Abstract SMT 2007 E-matching for Fun and Profit (2008)
Efficient handling of quantifiers is crucial for solving software verification problems. E-matching algorithms are used in satisfiability modulo theories solvers that handle quantified formulas...
Soundness and Completeness Warnings in ESC/Java2 ABSTRACT (2008)
Joseph R. Kiniry, Alan E. Morkan, Barry Denby
Usability is a key concern in the development of verification tools. In this paper, we present an usability extension for the verification tool ESC/Java2. This enhancement is not achieved through...
with contributions from (2008)
Joseph R. Kiniry, Patrice Chalin, Clément Hurlin, Cees-bart Breunesse, Julien Charles, ...
Automatic verification by means of extended static checking (ESC) has seen some success in industry and academia due to its lightweight and easy-to-use nature. Unfortunately, ESC comes at a cost: a...
David R. Cok, Joseph R. Kiniry, B Mc
Progress and issues in building and using ESC/Java2, including a case study involving the use of the tool to
with contributions from (2008)
Joseph R. Kiniry, Patrice Chalin, Clément Hurlin, Cees-bart Breunesse, David Cok, ...
Automatic verification by means of extended static checking (ESC) has seen some success in industry and academia due to its lightweight and easy-to-use nature. Unfortunately, ESC comes at a cost: a...
Formal Techniques for Java-like Programs (FTfJP) (2008)
Ro Coglio, Marieke Huisman, Joseph R. Kiniry, Peter Müller, Erik Poll
Abstract. This report gives an overview of the sixth Workshop on Formal
Joseph R. Kiniry, Joseph R. Kiniry, Group Members, Adam Rifkin, Roman Ginis, Dr. Paolo Sivilotti, ...
Special thanks go to my wonderful advisor, Dr. K. Mani Chandy. Thanks also to Infospheres
Kind Theory and Software Reuse (2007)
Joseph Kiniry Security, Joseph R. Kiniry
Kind theory is a logic for describing and reasoning about structured knowledge in communities.
B.: Soundness and Completeness Warnings in ESC/Java2 (2006)
Joseph R. Kiniry, Alan E. Morkan, Barry Denby
Usability is a key concern in the development of verification tools. In this paper, we present an usability extension for the verification tool ESC/Java2. This enhancement is not achieved through...
Beyond assertions: Advanced specification and verification with JML and ESC/Java2 (2006)
Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, Erik Poll
Abstract. Many state-based specification languages, including the Java Modeling Language (JML), contain at their core specification constructs familiar to most undergraduates: e.g., assertions, pre-...
Beyond assertions: Advanced specification and verification with JML and ESC/Java2 (2006)
Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, Erik Poll
Abstract. Many state-based specification languages, including the Java Modeling Language (JML), contain at their core specification constructs familiar to most undergraduates: e.g., assertions, pre-...
David R. Cok, Joseph R. Kiniry
Abstract. The ESC/Java tool was a lauded advance in effective static checking of realistic Java programs, but has become out-of-date with respect to Java and the Java Modeling Language (JML). The...
David R. Cok, Joseph R. Kiniry
Abstract. The ESC/Java tool was a lauded advance in effective static checking of realistic Java programs, but has become out-of-date with respect to Java and the Java Modeling Language (JML). The...
This paper describes the several user-interface features for interactive theorem provers. Many of these features mimic functionality that already exists, and have great utility, in modern interactive...
An overview of JML tools and applications (2004)
Lilian Burdy, Yoonsik Cheon, David R. Cok, Davidr. Cok, Michael D. Ernst, Joseph R. Kiniry, ...
The Java Modeling Language (JML) can be used to specify the detailed design of Java classes and interfaces by adding annotations to Java source files. The aim of JML is to provide a specification...
An Overview of JML Tools and Applications (2003)
Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph R. Kiniry, Gary T. Leavens, ...
The Java Modeling Language (JML) can be used to specify the detailed design of Java classes and interfaces by adding annotations to Java source files. The aim of JML is to provide a specification...
An overview of jml tools and applications (2003)
Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph R. Kiniry, Gary T, ...
original version is available at www.springerlink.com
Semantic component composition (2003)
Abstract. Building complex software systems necessitates the use of component-based architectures. In theory, of the set of components needed for a design, only some small portion of them are...
Semantic Component Composition (2002)
Building complex software systems necessitates the use of component-based architectures. In theory, of the set of components needed for a design, only some small portion of them are "custom"; the...
Monitoring and Debugging Concurrent and Distributed Object-Oriented Systems (2002)
A major part of debugging, testing, and analyzing a complex software system is understanding what is happening within the system at run-time. Some developers advocate running within a debugger to...
Semantic Properties for Lightweight Specification in Knowledgeable Development Environments (2002)
Semantic properties are domain-specific specification constructs used to augment an existing language with richer semantics. These properties are taken advantage of in system analysis, design,...
iii This thesis describes a theory for representing, manipulating, and reasoning about structured pieces of knowledge in open collaborative systems. The theory’s design is motivated by both its...
Semantic properties for lightweight specification in knowledgeable development environments (2002)
Abstract. Semantic properties are domain-specific specification constructs used to augment an existing language with richer semantics. These properties are taken advantage of in system analysis,...
iii This thesis describes a theory for representing, manipulating, and reasoning about structured pieces of knowledge in open collaborative systems. The theory’s design is motivated by both its...
Leading to a Kind Description Language: Thoughts on Component Specification (1999)
The Kind Description Language (KDL) is a language used for describing the interface and behavior of software components. KDL is an extension of the Object Management Group's Object Constraint...
Leading to a Kind Description Language: Thoughts on Component Specification (1999)
The Kind Description Language (KDL 1 ) is a language used for describing the interface and behavior of software components. KDL is an extension of the Object Management Group's Object Constraint...
Leading to a Kind Description Language: Thoughts on Component Specification (1999)
The Kind Description Language (KDL 1 ) is a language used for describing the interface and behavior of software components. KDL is an extension of the Object Management Group's Object Constraint...
CDL: A Component Description Language (1999)
Component Description Language (CDL 1 ) is a language used for describing the interface and behavior of software components. CDL is an extension of the Object Management Group's Object...
The Specification of Dynamic Distributed Component Systems (1998)
Modern computing systems are terribly complicated - so complex that most system designers and developers can only hope to understand their small piece of the larger project. The primary technologies...
A New Construct for Systems Modeling and Theory: The Kind (1998)
Our primary research goal is the development of theories and technology to facilitate the design, implementation, and management of complex systems. Complex systems, in this context, are any systems...
JPP: A Java Pre-Processor (1998)
Kiniry, Joseph R., Cheong, Elaine
The Java Pre-Processor, or JPP for short, is a parsing pre-processor for the Java programming language. Unlike its namesake (the C/C++ Pre-Processor, cpp), JPP provides functionality above and beyond...
IDebug: An Advanced Debugging Framework for Java (1998)
IDebug, the Infospheres debugging framework, is an advanced debugging framework for Java. This framework provides the standard core debugging and specification constructs such as assertions, debug...
A New Construct for Systems Modeling and Theory: The Kind (1998)
Our primary research goal is the development of theories and technology to facilitate the design, implementation, and management of complex systems. Complex systems, in this context, are any systems...
IDebug: An Advanced Debugging Framework for Java (1998)
IDebug, the Infospheres debugging framework, is an advanced debugging framework for Java. This framework provides the standard core debugging and specification constructs such as assertions, debug...
A Cottage Industry of Software Publishing: Implications for Theories of Composition (1998)
. This note explores the use of UNITY-based theories to facilitate a cottage industry of software publishing. The requirements for such an industry are discussed, the appropriateness of UNITY...
A New Construct for Systems Modeling and Theory: The Kind (1998)
Our primary research goal is the development of theories and technology to facilitate the design, implementation, and management of complex systems. Complex systems, in this context, are any systems...
JPP: A Java Pre-Processor (1998)
Joseph Kiniry And, Joseph R. Kiniry, Elaine Cheong
The Java Pre-Processor, or JPP for short, is a parsing pre-processor for the Java programming language. Unlike its namesake (the C/C++ Pre-Processor, cpp), JPP provides functionality above and beyond...
A Cottage Industry of Software Publishing: Implications for Theories of Composition (1998)
Mani Chandy Paolo, Joseph R. Kiniry
. This note explores the use of UNITY-based theories to facilitate a cottage industry of software publishing. The requirements for such an industry are discussed, the appropriateness of UNITY...
The Specification of Dynamic Distributed Component Systems (1998)
Joseph R. Kiniry, Joseph R. Kiniry, Group Members, Adam Rifkin, Roman Ginis, Dr. Paolo Sivilotti, ...
Modern computing systems are terribly complicated --- so complex that most system designers and developers can only hope to understand their small piece of the larger project. The primary...
JPP: A Java Pre-Processor (1998)
Joseph R. Kiniry, Elaine Cheong
The Java Pre-Processor, or JPP for short, is a parsing pre-processor for the Java programming language. Unlike its namesake (the C/C++ Pre-Processor, cpp), JPP provides functionality above and beyond...
A Cottage Industry of Software Publishing: Implications for Theories of Composition (1998)
. This note explores the use of UNITY-based theories to facilitate a cottage industry of software publishing. The requirements for such an industry are discussed, the appropriateness of UNITY...
A Cottage Industry of Software Publishing: Implications for Theories of Composition (1998)
K. Mani Chandy, Joseph R. Kiniry
. This note explores the use of UNITY-based theories to facilitate a cottage industry of software publishing. The requirements for such an industry are discussed, the appropriateness of UNITY...
IDebug: An advanced debugging framework for Java (1998)
The IDebug debugging framework is an advanced debugging framework for Java. This framework provides the standard core debugging and specification constructs such as assertions, debug levels and...
and Hanne Riis Nielson. 2-level -lifting (1988)
Joseph R. Kiniry, Alan E. Morkan, Dermot Cochran, Fintan Fairmichael, Patrice Chalin, Martijn Oostdijk, ...
Abstract. Remote internet voting incorporates many of the core challenges of trusted global computing. In this paper, we present the Kiezen op Afstand 4 (KOA) system. KOA is a Free Software, remote...