Johann Schumann's Publications

download (PostScript) or (PDF)

Automated Theorem Proving in Software Engineering

Fast Links:

2004  

2003 -- 2002 -- 2001 -- 2000 -- 1999 -- 1997 -- 1996 -- 1995 -- 1994 -- 1993 -- 1992 or earlier

Johann Schumann and Pramod Gupta
Monitoring the Performance of a neuro-adaptive Controller
In Proc. MAXENT 2004.

Karen A. Huyser, Kevin H. Knuth, Bernd Fischer, Johann Schumann, Domhnull Granquist-Fraser, and Arsen R. Hajian
Discovering Planetary Nebula Geometries: Explorations with a Hierarchy of Models
In Proc. MAXENT 2004.

Ewen Denney, Bernd Fischer, and Johann Schumann
Using Automated Theorem Provers to Certify Auto-Generated Aerospace Software
in Proc. IJCAR 2004.

Ewen Denney, Bernd Fischer, and Johann Schumann
Adding Assurance to Automatically Generated Code
in Proc. HASE 2004.

Pramod Gupta and Johann Schumann
A Tool for Verification and Validation of Neural Network Based Adaptive Controllers for High Assurance Systems
in Proc. HASE 2004.

Bernd Fischer and Johann Schumann
Automating the Analysis of Planetary Nebulae Images
In Proc ASE 2003.

Jon Whittle and Johann Schumann
Automating the Implementation of Kalman Filter Algorithms
submitted to ACM Journal of Mathematical Software, 2003.

Stacy Nelson and Johann Schumann
What makes a Code Review Trustworthy?
In Proc. HICSS-37.

Johann Schumann, Pramod Gupta and Stacy Nelson.
On Verification & Validation of Neural Network Based Controllers
In Proc. Engineering Applications of Neural Networks (EANN'03).

Gabriele Scheler and Johann Schumann.
Presynaptic modulation as fast synaptic switching: state-dependent modulation of task performance
In Proc. IJCNN, 2003

A.G. Gray, B. Fischer, J. Schumann, and W. Buntine.
Automatic derivation of statistical algorithms: The EM family and beyond
In Proc. NIPS-15, 2003

Johann Schumann, Bernd Fischer, Mike Whalen, and Jon Whittle.
Certification Support for Automatically Generated Programs
In Proc. HICSS'36, 2003

Bernd Fischer and Johann Schumann
AutoBayes: A System for Generating Data Analysis Programs from Statistical Models.
Journal Functional Programming, 2002 (in print).

.

Johann Schumann and Stacy Nelson.
Toward V&V of Neural Network Controllers.
In Proceedings Workshop on self-healing Systems (WOSS '02).

Mike Whalen, Johann Schumann, and Bernd Fischer.
Synthesizing Certified Code.
In Proceedings FME 2002, LNAI, Springer, 2002.

Mike Whalen, Johann Schumann, and Bernd Fischer.
Combining Program Synthesis with Automatic Code Cerification (System Description)
Conference on Automated Deduction (CADE) }, LNAI, Springer, 2002.

Jon Whittle and Johann Schumann.
Scenario-based Engineering of Multi-agent Systems.
In Chr.~Rouff (ed.), Formal Approaches to Agent-based Systems, Kluwer, 2002.

Bernd Fischer and Johann Schumann
Automated Synthesis of Statistical Data Analysis Programs
Proc. Workshop SDP (Science Data Processing) 2002, NASA Goddard, 2002.

Johann Schumann
Automatic Synthesis of Safety-Related Software
In Proc. AAAI Spring Symposium Series, 2002, Workshop on Logic-based Program Synthesis: State of the Art and Future Trends, AAAI, 2002.

Mike Whalen, Johann Schumann, and Bernd Fischer.
Synthesizing Certified Code.
RIACS Technical Report 02.03

 
Jon Whittle, Jeffrey Van Baalen, Johann Schumann, Peter Robinson, Tom Pressburger, John Penix, Phil Oh, Michael Lowry, and Guillaume Brat
Amphion/NAV: Deductive Synthesis of State Estimation
Robust Software Engineering, 2001

Johann Schumann and Peter Robinson
[] or SUCCESS is Not Enough: Current Technology and Future Directions in Proof Presentation
WS "Future Directions in Deduction", IJCAR 2001

Johann Schumann and Jon Whittle
Automatic Synthesis of UML Designs from Requirements in an Iterative Process
WS PMD'01 (Precise Modeling and Deduction for Object-oriented Software Development), invited lecture IJCAR 2001

Bernd Fischer, Tom Pressburger, Grigore Rosu, and Johann Schumann
The AutoBayes Porgam Synthesis System - System Description-
In. Proc. Calculemus 2001, 2001.

Johann Schumann and Jon Whittle
Automatic Synthesis of Agent Designs in UML
in Proc. FAABS, Springer, 2001.

Jon Whittle and Johann Schumann
Generating Statechart Designs From Scenarios
in Proc. ICSE. 2000.

Bernd Fischer and Johann Schumann
Generating Data Analysis Programs from Statistical Models
in Proc. SAIG, 2000.

Johann Schumann
Automatic Debugging Support for UML Designs
in M. Ducasse (ed), proceedings of the Fourth International Workshop on Automated Debugging (AADEBUG 2000), August 2000, Munich

 

Johann Schumann
PIL/SETHEO: A Tool for the Automatic Analysis of Authentication Protocols
in Proc. Computer Aided Verification (CAV), Springer, 1999.

Johann Schumann
Automatic Theorem Proving in High Quality Software Design
In Intellectica and Computational Logic - Papers in Honor of W. Bibe l, Kluwer 1999.

Johann Schumann
 Automatische Verifikation von Authentifikationsprotokollen.
KI 1998 (in German).

under construction

NORA/HAMMR: Making Deduction Based Component retrieval Practical
in Proc. ASE-12, 1997

Workshop of Automated Theorem Proving in Software Engineering
(ed.), during CADE-14, 1997

Automatic Verification of Cryptographic Protocols with SETHEO
in Proc. CADE-14, 1997

SETHEO Goes Software Engineering: Application of ATP to Software Reuse
in Proc. CADE-14, 1997

ILF-SETHEO: Processing Model Elimination Proof for Natural Language Output
in Proc. CADE-14, 1997

Automatic Verification of Cryptographic Protocols Using SETHEO
AR-Report, TU Muenchen, 1996

SiCoTHEO --- Simple Competitive parallel Theorem Provers based on SETHEO
Proc.~of PPAI'95, Montreal, Ca., 1995.

Using SETHEO for Verifying the Development of a Communication Protocol in Focus
- A Case Study -
Proc.~of Workshop Analytic Tableaux and Related Methods, Springer LNAI 918, pp 338-352,1995.

DELTA --- A Bottom-up Preprocessor for Top-Down Theorem Provers
Proc. CADE 12.

Tableaux-based Theorem Provers: Systems and Implementations
Journal of Automated Reasoning.

Analysing the Load Balancing Scheme of a Parallel System on Multiprocessors
Proc. PARLE 94.

Using SETHEO for verifying the development of a Communication
Protocol in FOCUS -- A Case Study --
long version, SFB Technical Report,SFB342/20/94A,TUM.

SETHEO V3.2: Recent Developments (System Abstract)
Proc. CADE 12.

Parallel Automated Theorem Proving
Parallel Processing for Artificial Intelligence I.

KPROP - An AND-parallel Theorem Prover for Propositional Logic implemented in KL1
Proc. Automated Deduction CADE--11.

PARTHEO}: a High Performance Parallel Theorem Prover
Proc. CADE 10, 1992.

Johann Schumann
Efficient Theorem Provers based on an Abstract Machine
Dissertation, Technische Universitaet Muenchen, Germany, 1991. (gzipped Postscript)

---

Johann Schumann , 1997-03-02

Information and Papers