A selection of publications, thematically sorted, is given below.

Design of Safety-Critical or Dependable Systems

• H. Hungar. Assuring Standard Conformance of Partial Interfaces. In: Proc. Verification and Assurance 2013, to appear.
• H. Hungar and M. Behrens. Opening Up the Verification and Validation of Safety-Critical Software. In: Proc. ZeMoSS 2013, to appear.
• W. Damm, H. Hungar, B. Josko, T. Peikenkamp, I. Stierand. Using contract-based component specifications for virtual integration testing and architecture design. In: Lukasiewycz, Chakraborty, Milbredt, eds., DATE 2011, pp 1-6. IEEE, 2011.
• M. Fränzle, T. Gezgin, H. Hungar, S. Puch, G. Sauter. Using guided simulation to assess driver assistance systems. In: E. Schnieder and G. Tarnai, Eds., Proc. FORMS/FORMAT 2010, Springer, pp 195-206, 2010.
• H. Hungar, M. Huhn. Using UML for Software safety and Certification - Model-based development of safety-critical software-intensive systems. In: Giese, Karsai, Lee, Rumpe, Schätz: Model-Based Engineering of Embedded Real-Time Systems, LNCS 6100, pp 201-227.
• H. Hungar, G. Bruhns, O. Plan and O. Lemke. OPRAIL - Normenkonforme Entwicklung sicherheitsrelevanter Software unter Einsatz der UML. Signal+Draht 07, 2007.
• H. Hungar, O. Robbe and B. Wirtz. Safe-UML - Restricting UML for the development of safety-critical systems. In: E. Schnieder and G. Tarnai, Eds., Proc. FORMS/FORMAT 2007, pp 467-475, 2007.
• W. Damm, H. Hungar and E.-R. Olderog. Verication of cooperating traffic agents. Int. J. Control, 79(5):395-421, 2006.

• H. Hungar. Compositionality with Strong Assumptions. In: P. Petterson and C. Seceleanu, Eds., Proc.\ 23rd Nordic Workshop on Programming Theory, TR 254/2011, Mälardalen University, pp 11-13, 2011.

• H. Hungar and B. Steffen. Behavior-based model construction. Software Tools for Technology Transfer, 4:1-11, 2004.
• H. Hungar, T. Margaria and B. Steffen. Test-based model generation for legacy systems. In: IEEE International Test Conference, 2003.
• A. Hagerer, H. Hungar, O. Niese and B. Steffen. Model g eneration by moderated regular extrapolation. In: R.-D. Kutsche and H. Weber, Eds., Proc. Fundamental Approaches to Software Engineering 2002, LNCS2306, pp 80-95.Springer,2002.

Infinite Systems: Recursion

• H. Hungar. Model checking and higher-order recursion. In: M. Kutylowski, L. Pacholski and Thomasz Wierzbicki, Eds., 24th Conf. on Math. Found. of Comp. Sc., LNCS 1672, pp 149-159, 1999.
• H. Hungar and B. Steffen. Local model checking for context-free processes. Nordic J. of Comp., 1:364-385, 1994.
• H. Hungar. Model checking of macro processes. In: D.L. Dill, Ed., 6th Int. Conf. on Computer Aided Verication, LNCS 818, pp 169-181, 1994.
• H. Hungar. Beyond finite-state model checking: Verifying large and infinite systems. Habilitation Thesis, CvO University Oldenburg, 1998.

• W. Damm, S. Disch, H. Hungar, S. Jacobs, J. Pang, F. Pigorsch, C. Scholl, U. Waldmann and B. Wirtz. Exact state representations in the verification of linear hybrid systems with large discrete state space. In: Proc. 5th Int. Symp. Automated Technology for Verification and Analysis, LNCS 4762, pp 425-440, 2007.
• W. Damm, S. Disch, H. Hungar, J. Pang, F. Pigorsch, C. Scholl, U. Waldmann and B. Wirtz. Automatic verication of hybrid systems with large discrete state space. In: Proc. 4th Int. Symp. on Automated Technology for Verication and Analysis, LNCS 4218, pp 276-291, 2006.
• J. Bohn, W. Damm, O. Grumberg, H. Hungar and K. Laster. First-order CTL model checking. In V.Arvind and R.Ramanujam, Eds., 18th Conf. on Foundations of Software Technology and Theoretical Comp. Sc., LNCS 1530, pp 283-294, 1998.
• H. Hungar, O. Grumberg and W. Damm. What if model checking must be truly symbolic. In: P. Camurati and H. Eveking, Eds., Conf. on Correct Hardware Design and Verification Methods, LNCS 987, pp 1-20, 1995.

• H. Hungar. Beyond finite-state model checking: Verifying large and infinite systems (Part II). Habilitation Thesis,CvO University Oldenburg, 1998.
• H. Hungar. Specification and verification using a visual formalism on top of temporal logic. In: M. Broy, S. Merz and K. Spies, Eds., Formal Systems Specification: The RPC-Memory Specification Case Study, LNCS 1169, pp 305-339, 1996.
• J. Bohn and H. Hungar. Traverdi - transformation and verification of distributed systems. In: M. Broy and S. Jähnichen, Eds., KORSO: Methods, Languages, and Tools for the Construction of Correct Software, LNCS1009, pp 317-338, 1995.
• H. Hungar. Combining model checking and theorem proving to verify parallel processes. In: C. Courcoubetis, Ed., 5th Int. Conf. on Computer Aided Verication, LNCS 697, pp 154-165, 1993.

• T. Bienmuller, U. Brockmeyer, W. Damm, G. Döhmen, C. Eßmann, H. Holberg, H. Hungar, B. Josko, R. Schlör, G. Wittich, H. Wittke, G. Clements, J. Rowlands and E. Sefton. Formal verification of an avionics application using abstraction on symbolic model-checking. In: F. Redmill and E. Sefton, Eds., Towards system safety. Seventh Safety-critical Systems Symp., pp. 150-173. Springer,1999.
• W. Damm, B. Josko, H. Hungar and A. Pnueli. A compositional real-time semantics of Statemate designs. In: W.-P. de Roever, H. Langmaack and A. Pnueli, Eds., Compositionality - The Significant Difference, LNCS 1536, pp 186-238, 1998.

• H. Hungar. Expressibility of the semantics of sequential programs in first-order logic. Fundamenta Informatica, 21:345-366, 1994.
• H. Hungar. Complexity bounds of Hoare-style proof systems. In: 6th IEEE Symp. on Logic in Comp. Sc., pp 120-126, 1991.
• H. Hungar. Complexity of proving program correctness. In: T. Ito and A.R. Meyer, Eds., Theoretical Aspects of Computer Software, LNCS 526, pp 459-474, 1991.
• H. Hungar. Über Komplexitätsfragen Hoarescher Beweissyteme: Effiziente Beweiserstellung und komplexitätsbedingte Grenzen bestimmter Systeme. Technical Report 9007, CAU Kiel, 1990. Dissertation.
• M. Grabowski and H. Hungar. On the existence of effective Hoare logics. In: 3rd Symp. Logic in Comp. Sc., pp 428-435, 1988.
• H. Hungar. Untersuchungen über die Ausdruckskraft von logischen Formeln bezüglich des Ein/Ausgabeverhaltens von Programmen. Master Thesis, CAU Kiel, 1985.