NASA Logo, National Aeronautics and Space Administration

Johann Schumann's Publications


Book

Automated Theorem Proving in Software Engineering

Papers and Technical Reports



2010

J. Schumann, K. Cate, and A. Lee
Parametric Analysis of Air Traffic Track Data with the AutoBayes Synthesis System.
Proc. LOPSTR 2010. RISC TR. (will be published in LNCS 2011).

A. Srivastava and J. Schumann
The Case for Software Health Management
IEEE Computer (under review), 2010.

J. Schumann, O. Mengshoel, A. Srivastava and A. Darwiche.
Towards Software Health Management with Bayesian Networks.
In Proc. FSE (Future of Software Engineering), SDP, 2010.

J. Schumann, A. Bajwa, P. Berg, and R.
Towards Thirumalainambi Parametric Testing of Launch Vehicle FDDR Models
In AIAA Space, 2010.

J. Schumann, A. Srivastava and O. Mengshoel
Who guards the Guardians? — Toward V&V of Health Management Software (Short Paper)
In Proc. Runtime Verification (RV) 2010, Springer.

D, Giannakopoulou, D. Bushnell, and J. Schumann
Formal Testing for Separation Assurance Accepted
for AMAI (special issue Formal Methods in Aerospace), 2010.

J. Schumann, P. Gupta, and Y.Liu.
Application of Neural Networks in High Assurance Systems: A Survey Chapter 1 of J. Schumann, Y. Liu, editors, Applications of Neural Networks in High Assurance Systems,
pp 1–40, Springer, 2010.

2009

C. Pasareanu, J. Schumann, P. Mehlitz, M. Lowry, G. Karsai, H. Nine, and S. Neema.
Model based Analysis and Test generation for Flight Software.
In Proc. SMC-IT, 2009

K. Pipatsrisawat, A. Darwiche, O. Mengshoel, and J. Schumann.
Software Health Management: A Short Review of Challenges and Existing Techniques.
In Workshop Software Health Management, SMC-IT, 2009.

J. Schumann, K. Gundy-Burlet, C. P˘as˘areanu, T. Menzies, and T. Barrett.
Software V&V Support by Parametric Analysis of Large Software Simulation Systems.
Proc. IEEE Aerospace, IEEE, 2009.

2008

J. Schumann, K. Gundy-Burlet, C. P˘as˘areanu, T. Menzies, and T. Barrett.
Tool Support for Parametric Analysis of Large Software Simulation Systems
Proceedings Automated Software Engineering (ASE), 2008.

Y. Liu, J. Schumann, and B. Cukic.
Statistical Evaluation Methods for V&V of Neuro-Adaptive Systems In W. Eric Wong, B. Cukic, eds.,
An Adaptive Control Approach for Software Quality Improvement, World Scientific Press, 2008 (in print).

K. Gundy-Burlet, J. Schumann, T. Menzies, and T Barrett.
Parametric Analysis of ANTARES Re-entry Guidance Algorithms Using Advanced Test Generation and Data Analysis.
Proc. iSAIRAS 2008 (9th International Symposium on Artifical Intelligence, Robotics and Automation in Space), 2008.

2007

J. Schumann and Y. Liu.
Tools and Methods for the Verification and Validation of Adaptive Aircraft Control Systems.
IEEE Aerospace Conference, IEEE Press, 2007.

J. Schumann and E. Denney.
Automatic Generation of Certifiable Space Communication Software.
IEEE Aerospace Conference, IEEE Press, 2007.

2006

J. Schumann and Y. Liu.
Performance Estimation of a Neural Network-based Controller.
International Symposium on Neural Networks (ISNN), Chengdu, China, Springer Verlag, 981–990, 2006.

E. Denney, B. Fischer, and J. Schumann.
An Empirical Evaluation of Automated Theorem Provers in Software Certification.
InternationalJournal on Artificial Intelligence Tools 15(1):81–108, 2006.

J. Schumann and W. Visser.
Autonomy Software: V&V Challenges and Characteristics.
IEEE Aerospace Conference, IEEE Press, 2006.

C. Tseng, P. Gupta, and J. Schumann.
Performance analysis using a Fuzzy rule base representation of the Cooper-Harper rating.
IEEE Aerospace Conference, IEEE Press, 2006.

2005

S. Jacklin, J. Schumann, P. Gupta, M. Richard, K. Guenther, and F. Soares.
Development of Advanced Verification and Validation Procedures and Tools for the Certification of Learning Systems in Aerospace Applications.
Infotech at Aerospace, AIAA, 2005.

A. Srivastava, J. Schumann, and B. Fischer.
An Ensemble Approach to Building Mercer Kernels with Prior Information.
IEEE SMC Conference, IEEE 2005.

P. Gupta, K. Guenther, J. Hodgkinson, S. Jacklin, M. Richard, J. Schumann, and F. Soares.
Performance Monitoring and Assessment of Neuro-Adaptive Controllers for Aerospace Applications Using a Bayesian Approach. Guidance.
Navigation and Control (GNC) Conference, AIAA 2005-6451, 2005.

J. Schumann, P. Gupta, and S. Jacklin.
Toward Verification and Validation of Adaptive Aircraft Controllers.
IEEE Aerospace Conference, IEEE Press, 2005.

E. Denney, B. Fischer, J. Schumann, and J. Richardson.
Automatic Certification of Kalman Filters for Reliable Code Generation.
IEEE Aerospace Conference, IEEE Press, 2005.

J. Richardson, J. Schumann, B. Fischer, and E. Denney.
Rapid Exploration of the Design Space During Automatic Generation of Kalman Filter Code.
IEEE Aerospace Conference, IEEE Press, 2005.

2004

P. Gupta, K. Loparo, J. Schumann, and F. Soares.
Verification and Validation Methodology of Real-Time Adaptive Neural Networks for Aerospace Applications.
International Conference on Computational Intelligence for Modeling, Control, and Automation, 2004.

S. Jacklin, M. Lowry, J. Schumann, P. Gupta, J. Bosworth, E. Zavala, J. Kelly, K. Hayhurst, C. Belcastro, and C. Belcastro.
Verification, Validation and Certification Challenges for Adaptive Flight Control Systems Software.
AIAA Guidance Navigation and Control Conference and Exhibit, 2004.

K. Huyser, K. Knuth, B. Fischer, J. Schumann, D, Granquist-Fraser, A. Hajian.
Discovering Planetary Nebula Geometries: Explorations with a Hierarchy of Models.
In Proc. MAXENT 2004, AIP Conference Proceedings 735, pp 135–142, Americal Institute of Physics, 2004.

J. Schumann and P. 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.


2003

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
In Proc. 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

2002

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

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

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


2001

 
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
"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.


2000

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


 

1999

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.


1998

Johann Schumann
 Automatic verification of authentication protocols
KI 1998 (in German).

1997

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


1996

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


1995

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

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


1994

DELTA --- A Bottom-up Preprocessor for Top-Down Theorem Provers
In 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
In 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)
In Proc. CADE 12.


1993

Parallel Automated Theorem Proving
In Proc. Parallel Processing for Artificial Intelligence I.


1992

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

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


First Gov logo
NASA Logo - nasa.gov