Bernd Finkbeiner
Prof. Bernd Finkbeiner, Ph.D. is a faculty member at the CISPA Helmholtz Center for Information Security and a professor of computer science at Saarland University. He obtained his Ph.D. in 2003 from Stanford University. Since 2003, he leads the Reactive Systems Group, which became part of CISPA in 2020. His research focus is the development of reliable guarantees for the safety and security of computer systems, including specification, program synthesis and repair, and static and dynamic verification. Major projects include output-sensitive algorithms for reactive synthesis (➠ OSARES), logics and algorithms for hyperproperties (➠ HYPER), and the stream-based monitoring of cyber-physical systems (➠ RTLOLA).
Project HYPER
Logics and Algorithms for a Unified Theory of Hyperproperties
ERC Advanced Grant 2022-2027
Contact
CISPA Helmholtz Center for Information Security
phone: +49 681 870832059
eMail: finkbeiner at cispa.de
Teaching
- Winter 2024/25: Automata, Games and Verification (advanced lecture)
The theory of automata over infinite objects provides a succinct, expressive, and formal framework for reasoning about reactive systems, such as communication protocols and control systems. Reactive systems are characterized by their nonterminating behaviour and persistent interaction with their environment. In this course we will study the main ingredients of this elegant theory, and its application to automatic verification (model checking) and program synthesis.
Tutorial videos
- Hyperproperties (30 minutes. Isaac Newton Institute for Mathematical Sciences, Cambridge)
- Reactive Synthesis (120 minutes. Simons Institute, Berkeley)
Overview papers
Künstliche Intelligenz in der Softwareentwicklung: Über die Schulter geschaut.
iX Magazin für professionelle Informationstechnik 8/2021 (in German)
iX Magazin für professionelle Informationstechnik 8/2021 (in German)
Publications
For an up-to-date list of publications see DBLP.
- Checking Satisfiability of Hyperproperties using First-Order Logic. With Raven Beutner. ATVA 2024
- A Tutorial on Stream-Based Monitoring. With Jan Baumeister, Florian Kohn, and Frederik Scheerer. FM 2024
- Visualizing Game-Based Certificates for Hyperproperty Verification. With Raven Beutner, and Angelina Göbl. FM 2024
- Information Flow Guided Synthesis with Unbounded Communication. With Niklas Metzger and Yoram Moses. CAV 2024
- Syntax-Guided Automated Program Repair for Hyperproperties. With Raven Beutner, Tzu-Han Hsu, and Borzoo Bonakdarpour. CAV 2024
- Monitoring Unmanned Aircraft: Specification, Integration, and Lessons-Learned. Jan Baumeister, Florian Kohn, Florian Löhr, Guido Manfredi, Sebastian Schirmer, and Christoph Torens. CAV 2024
- Synthesis of Temporal Causality. With Hadar Frenkel, Niklas Metzger, and Julian Siber. CAV 2024
- Temporal Behavior Trees: Robustness and Segmentation. With Sebastian Schirmer, Jasdeep Singh, Emily Jensen, Johann Dauer, and Sriram Sankaranarayanan. HSCC 2024
- Temporal Behavior Trees -— Segmentation. With Sebastian Schirmer, Jasdeep Singh, Emily Jensen, Johann Dauer, and Sriram Sankaranarayanan. HSCC 2024
- Non-Deterministic Planning for Hyperproperty Verification. With Raven Beutner. ICAPS 2024
- Hyper Strategy Logic. With Raven Beutner. AAMAS 2024
- Monitoring Second-Order Hyperproperties. With Raven Beutner, Hadar Frenkel, and Niklas Metzger. AAMAS 2024
- On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing. With Raven Beutner. AAAI 2024
Concurrent Hyperproperties. With Ernst-Rüdiger Olderog. Theories of Programming and Formal Methods 2023 - Leveraging Static Analysis: An IDE for RTLola. With Florian Kohn and Malte Schledjewski. ATVA 2023
- Reactive Synthesis of Smart Contract Control Flows. With Jana Hofmann, Florian Kohn, and Noemi Passing. ATVA 2023
- Checking and Sketching Causes on Temporal Sequences. With Raven Beutner, Hadar Frenkel, and Julian Siber. ATVA 2023
- Logics and Algorithms for Hyperproperties. ACM SIGLOG News 2023
- Second-Order Hyperproperties. With Raven Beutner, Hadar Frenkel, and Niklas Metzger. CAV 2023
- Model Checking Omega-Regular Hyperproperties with AutoHyperQ. With Raven Beutner. LPAR 2023
- Counterfactuals Modulo Temporal Logics. With Julian Siber. LPAR 2023
- HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems. With Raven Beutner. LMCS 2023
- Automata-Based Software Model Checking of Hyperproperties. With Hadar Frenkel, Jana Hofmann, and Janine Lohse. NFM 2023
- Iterative Circuit Repair Against Formal Specifications With Matthias Cosler, Frederik Schmitt, and Christopher Hahn. ICLR 2023
- AutoHyper: Explicit-State Model Checking for HyperLTL. With Raven Beutner. TACAS 2023
- Smart Contract Synthesis Modulo Hyperproperties. With Norine Coenen, Jana Hofmann, and Julia Tillman. CSF 2023
- Synthesizing Dominant Strategies for Liveness. With Noemi Passing. FSTTCS 2022
- Temporal Causality in Reactive Systems. With Norine Coenen, Hadar Frenkel, Christopher Hahn, Niklas Metzger, and Julian Siber. ATVA 2022
- Information Flow Guided Synthesis. With Niklas Metzger and Yoram Moses. CAV 2022
- Explaining Hyperproperty Violations. With Norine Coenen, Raimund Dachselt, Hadar Frenkel, Christopher Hahn, Tom Horak, Niklas Metzger, and Julian Siber. CAV 2022
- Software Verification of Hyperproperties Beyond k-Safety. With Raven Beutner. CAV 2022
- Prophecy Variables for Hyperproperty Verification. With Raven Beutner. CSF 2022
- Deciding Hyperproperties Combined with Functional Specifications. With Raven Beutner, David Carral, Jana Hofmann, and Markus Krötzsch. LICS 2022
- Can reactive synthesis and syntax-guided synthesis be friends? With Wonhyuk Choi, Ruzica Piskac, and Mark Santolucito. PLDI 2022
- BOCoSy: Small but Powerful Symbolic Output-Feedback Control. With Kaushik Mallik, Noemi Passing, Malte Schledjewski, Anne-Kathrin Schmuck. HSCC 2022
- Monitoring with Verified Guarantees. With Jan Baumeister, Johann C. Dauer, Sebastian Schirmer. STTT 2022
- A Truly Robust Signal Temporal Logic: Monitoring Safety Properties of Interacting Cyber-Physical Systems under Uncertain Observation. With Martin Fränzle, Florian Kohn, and Paul Kröger. Algorithms 2022
- Compositional synthesis of modular systems. With Noemi Passing. ISSE 2022
- Temporal Stream Logic modulo Theories. With Philippe Heim and Noemi Passing. FoSSaCS 2022
- Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory. With Manuel Gieseking, Jesko Hecking-Harbusch, and Ernst-Rüdiger Olderog. CSL 2022
- Linear-time Temporal Logic with Team Semantics: Expressivity and Complexity. With Jonni Virtema, Jana Hofmann, Juha Kontinen, and Fan Yang. FSTTCS 2021
- Neural Circuit Synthesis from Specification Patterns. With Frederik Schmitt, Christopher Hahn, and Markus N. Rabe. NeurIPS 2021.
- Monitoring with Verified Guarantees. With Johann C. Dauer and Sebastian Schirmer. RV 2021
- Visual Analysis of Hyperproperties for Understanding Model Checking Results. With Tom Horak, Norine Coenen, Niklas Metzger, Christopher Hahn, Tamara Flemisch, Julián Méndez, Dennis Dimov, and Raimund Dachselt. VIS 2021
- Runtime Enforcement of Hyperproperties. With Norine Coenen, Christopher Hahn, Jana Hofmann, and Yannick Schillo. ATVA 2021
- Live Synthesis. With Felix Klein and Niklas Metzger. ATVA 2021
- Compositional Synthesis of Modular Systems. With Noemi Passing. ATVA 2021
- Deep Learning for Temporal Logics. With Frederik Schmitt, Christopher Hahn, Jens U. Kreber, and Markus N. Rabe. AITP 2021
- A Temporal Logic for Strategic Hyperproperties. With Raven Beutner. CONCUR 2021
- Causality-Based Game Solving. With Christel Baier, Norine Coenen, Florian Funke, Simon Jantsch, and Julian Siber. CAV 2021
- A Temporal Logic for Asynchronous Hyperproperties. With Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour, and Cesar Sanchez. CAV 2021
- Specification Decomposition for Reactive Synthesis. With Gideon Geier and Noemi Passing. NFM 2021
- Automatic Optimizations for Runtime Verification Specifications. With Jan Baumeister, Matthis Kruse, Stefan Oswald, Noemi Passing, and Maximilian Schwenger. MT-CPS 2021
- Robust Monitoring for Medical Cyber-Physical Systems. With Andreas Keller, Jessica Schmidt, and Maximilian Schwenger. MedCPS 2021
- Teaching Temporal Logics to Neural Networks. With Christopher Hahn, Frederik Schmitt, Jens U. Kreber, and Markus N. Rabe. ICLR 2021
- RTLola on Board: Testing Real Driving Emissions on your Phone. With Sebastian Biewer, Holger Hermanns, Maximilian A. Köhl, Yannik Schnitzer, and Maximilian Schwenger. TACAS 2021
- Probabilistic Hyperproperties of Markov Decision Processes. With Rayna Dimitrova and Hazem Torfah. ATVA 2020
- Model Checking Branching Properties on Petri Nets with Transits. With Manuel Gieseking, Jesko Hecking-Harbusch and Ernst-Rüdiger Olderog. ATVA 2020
- Explainable Reactive Synthesis. With Tom Baumeister and Hazem Torfah. ATVA 2020
- Dependency-Based Compositional Synthesis. With Noemi Passing. ATVA 2020
- Realizing Omega-regular Hyperproperties. With Christopher Hahn, Jana Hofmann, and Leander Tentrup. CAV 2020
- Verified Rust Monitors for Lola Specifications. With Stefan Oswald, Noemi Passing, and Maximilian Schwenger. RV 2020
- Automatic Optimizations for Stream-based Monitoring Languages. With Jan Baumeister, Matthis Kruse, and Maximilian Schwenger. RV 2020
- RTLola Cleared for Take-Off: Monitoring Autonomous Aircraft. With Jan Baumeister, Sebastian Schirmer, Maximilian Schwenger, and Christoph Torens. CAV 2020
- AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL. With Manuel Gieseking, Jesko Hecking-Harbusch, and Ernst-Rüdiger Olderog. CAV 2020
- Controller Synthesis for Hyperproperties. With Borzoo Bonakdarpour. CSF 2020
- Efficient Monitoring of Hyperproperties using Prefix Trees. With Christopher Hahn, Marvin Stenger, and Leander Tentrup. STTT 2020
- How to Win First-Order Safety Games. With Helmut Seidl and Christian Müller. VMCAI 2020
- Synthesis from Hyperproperties. With Christopher Hahn, Philip Lukert, Marvin Stenger, and Leander Tentrup. Acta Informatica 2019
- Monitoring Hyperproperties. With Christopher Hahn, Marvin Stenger, and Leander Tentrup. FMSD 2019
- Approximate Automata for Omega-regular Languages. With Rayna Dimitrova and Hazem Torfah. ATVA 2019
- Model Checking Data Flows in Concurrent Network Updates. With Manuel Gieseking, Jesko Hecking-Harbusch, and Ernst-Rüdiger Olderog. ATVA 2019
- Program Repair for Hyperproperties.. With Borzoo Bonakdarpour. ATVA 2019
- On the Similarities of Aircraft and Humans: Monitoring CPS with StreamLAB. With Jan Baumeister, Maximilian Schwenger, and Hazem Torfah. CyberCardia 2019
- FPGA Stream-Monitoring of Real-time Properties. With Jan Baumeister, Maximilian Schwenger, and Hazem Torfah. EMSOFT 2019
- Synthroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications. With Gideon Geier, Philippe Heim, and Felix Klein. FMCAD 2019
- The Hierarchy of Hyperlogics. With Norine Coenen, Christopher Hahn, and Jana Hofmann. LICS 2019
- Synthesizing Approximate Implementations for Unrealizable Specifications. With Rayna Dimitrova and Hazem Torfah. CAV 2019
- Temporal Stream Logic: Synthesis beyond the Bools. With Felix Klein, Ruzica Piskac, and Mark Santolucito. CAV 2019
- StreamLAB: Stream-based Monitoring of Cyber-physical Systems. With Peter Faymonville, Malte Schledjewski, Maximilian Schwenger, Marvin Stenger, Leander Tentrup, Hazem Torfah. CAV 2019
- Verifying Hyperliveness. With Norine Coenen, Leander Tentrup, and Cesar Sanchez. CAV 2019
- Canonical Representations of k-Safety Hyperproperties. With Lennart Haas and Hazem Torfah. CSF 2019
- Real-time Stream Monitoring with StreamLAB. With Peter Faymonville, Malte Schledjewski, Maximilian Schwenger, Leander Tentrup, and Hazem Torfah. MT-CPS 2019
- Bounded Synthesis of Reactive Programs. With Carsten Gerstacker and Felix Klein. ATVA 2018
- MGHyper: Checking Satisfiability of HyperLTL formulas beyond the exists-forall Fragment. With Christopher Hahn and Tobias Hans. ATVA 2018
- Synthesizing Reactive Systems from Hyperproperties. With Christopher Hahn, Philip Lukert, Marvin Stenger, and Leander Tentrup. CAV 2018
- Model Checking Quantitative Hyperproperties. With Christopher Hahn and Hazem Torfah. CAV 2018
- The Complexity of Monitoring Hyperproperties. With Borzoo Bonakdarpour. CSF 2018
- RVHyper: A Runtime Verification Tool for Temporal Hyperproperties. With Christopher Hahn, Marvin Stenger, and Leander Tentrup. TACAS 2018
- Symmetric Synthesis. With Ruediger Ehlers. FSTTCS 2017
- Synthesis in Distributed Environments. With Paul Gölz. FSTTCS 2017
- Verifying Security Policies in Multi-agent Workflows with Loops. With Christian Müller, Eugen Zalinescu, and Helmut Seidl. CCS 2017
- Reactive Synthesis: Towards Output-Sensitive Algorithms. With Felix Klein. Dependable Software Systems Engineering 2017
- Causality-based Model Checking. With Andrey Kupriyanov. Invited paper. CREST 2017
- Temporal Hyperproperties. Bulletin of EATCS No 123, October 2017
- Density of Linear-time Properties. With Hazem Torfah. ATVA 2017
- Monitoring Hyperproperties. With Christopher Hahn, Marvin Stenger, and Leander Tentrup. RV 2017
- Stream Runtime Monitoring on UAS. With Florian-Michael Adolf, Peter Faymonville, Sebastian Schirmer, and Christoph Torens. RV 2017
- EAHyper: Satisfiability, Implication, and Equivalence Checking of Hyperproperties. With Christopher Hahn and Marvin Stenger. CAV 2017
- BoSy: An Experimentation Framework for Bounded Synthesis. With Peter Faymonville and Leander Tentrup. CAV 2017
- Vehicle Platooning Simulations with Functional Reactive Programming. With Felix Klein, Ruzica Piskac and Mark Santolucito. SCAV@CPSWeek 2017
- Is your software on dope? ⋆ Formal analysis of surreptitiously “enhanced” programs. With Pedro R. D’Argenio, Gilles Barthe, Sebastian Biewer, and Holger Hermanns. ESOP 2017
- Encodings of Bounded Synthesis. With Peter Faymonville, Markus N. Rabe, and Leander Tentrup, TACAS 2017
- The First-Order Logic of Hyperproperties. With Martin Zimmermann, STACS 2017
- Petri games: Synthesis of distributed systems with causal memory. With Ernst-Rüdiger Olderog. Information & Computation, 2017
- Facets of Software Doping. With Gilles Barthe, Pedro R. D’Argenio, and Holger Hermanns. ISOLA 2016
- A Stream-based Specification Language for Network Monitoring. With Peter Faymonville, Sebastian Schirmer, and Hazem Torfah. RV 2016
- What You Really Need To Know About Your Neighbor. With Werner Damm and Astrid Rakow. SYNT 2016
- Deciding Hyperproperties. With Christopher Hahn. CONCUR 2016
- Specifying and Verifying Secrecy in Workflows with Arbitrarily Many Agents. With Helmut Seidl and Christian Müller. ATVA 2016
- Synthesizing Skeletons for Reactive Systems. With Hazem Torfah. ATVA 2016
- Bounded Cycle Synthesis. With Felix Klein. CAV 2016
- Synthesis of Reactive Systems. Dependable Software Systems Engineering
- Bounded Synthesis for Petri Games. Correct System Design 2015
- Detecting Unrealizability of Distributed Fault-tolerant Systems. With Leander Tentrup. LMCS 2015
- Algorithms for Model Checking HyperLTL and HyperCTL*. With Markus Rabe and César Sánchez. CAV 2015
- ADAM: Causality-Based Synthesis of Distributed Systems. With Manuel Gieseking and Ernst-Rüdiger Olderog. CAV 2015
- Petri Games: Synthesis of Distributed Systems with Causal Memory. With Ernst-Rüdiger Olderog. GANDALF 2014
- Fast DQBF Refutation. With Leander Tentrup. SAT 2014
- Causal Termination of Multi-threaded Programs. With Andrey Kupriyanov. CAV 2014
- Automatic Compositional Synthesis of Distributed Systems. With Werner Damm. FM 2014
- Detecting Unrealizable Specifications of Distributed Systems. With Leander Tentrup. TACAS 2014
- Temporal Logics for Hyperproperties. With Michael R. Clarkson, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and Cesar Sanchez. POST 2014
- Counting Models of Linear-time Temporal Logic. With Hazem Torfah. LATA 2014
- Monitoring Parametric Temporal Logic. With Peter Faymonville and Doron Peled. VMCAI 2014
- Relational Abstract Interpretation for the Verification of 2-Hypersafety Properties. With Máté Kovács and Helmut Seidl. CCS 2013
- Bounded Synthesis. With Sven Schewe. STTT 2013
- Causality-Based Verification of Multi-threaded Programs. With Andrey Kupriyanov. CONCUR 2013
- A Temporal Logic for Hyperproperties. With Markus N. Rabe and César Sánchez. arXiv
- Lossy Channel Games under Incomplete Information. With Rayna Dimitrova. SR 2013
- Efficient Parallel Path Checking for Linear-Time Temporal Logic With Past and Bounds. With Lars Kuhtz. LMCS 2012
- Monitoring Temporal Information Flow with Rayna Dimitrova and Markus N. Rabe, ISOLA 2012
- The Complexity of Bounded Synthesis for Timed Control with Partial Observability with Hans-Jörg Peter, FORMATS 2012
- Counterexample-guided Synthesis of Observation Predicates with Rayna Dimitrova, FORMATS 2012
- Template-based Controller Synthesis for Timed Systems. With Hans-Jörg Peter. TACAS 2012
- Lazy Synthesis. With Swen Jacobs. VMCAI 2012
- Model Checking Information Flow in Reactive Systems. With Rayna Dimitrova, Máté Kovács, Markus N. Rabe, and Helmut Seidl. RS3 Best Paper Award. VMCAI 2012
- Monitoring Realizability. With Rüdiger Ehlers. RV 2011
- Weak Kripke Structures and LTL. With Lars Kuhtz. CONCUR 2011
- Does It Pay to Extend the Perimeter of a World Model? With Werner Damm. FM 2011
- Reactive Safety. With Rüdiger Ehlers. GANDALF 2011
- On the Virtue of Patience: Minimizing Büchi Automata. With Rüdiger Ehlers. SPIN 2010
- Model Checking the FlexRay Physical Layer Protocol. With Michael Gerke, Rüdiger Ehlers, and Hans-Jörg Peter. FMICS 2010
- Coordination Logic. With Sven Schewe. CSL 2010
- Synthesising Certificates in Networks of Timed Automata. With Hans-Jörg Peter and Sven Schewe. IET Software 2010
- SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems. TACAS 2010
- Synthesis of Fault-Tolerant Distributed Systems. With Rayna Dimitrova. ATVA 2009
- LTL Path Checking is Efficiently Parallelizable. With Lars Kuhtz. Best Paper Award. ICALP 2009
- Monitor Circuits for LTL with Bounded and Unbounded Future. With Lars Kuhtz. RV 2009
- Slicing Abstractions. With Ingo Brückner, Klaus Dräger, and Heike Wehrheim. FI 2008.
- Abstraction Refinement for Games with Incomplete Information. With Rayna Dimitrova. FSTTCS 2008
- Synthesizing Certificates in Networks of Timed Automata. With Hans-Jörg Peter and Sven Schewe. RTSS 2008
- Directed Model Checking with Distance-preserving Abstractions. With Klaus Dräger and Andreas Podelski. STTT 2008
- Subsequence Invariants. With Klaus Dräger. CONCUR 2008
- RESY: Requirement Synthesis for Compositional Model Checking. With Hans-Jörg Peter and Sven Schewe. TACAS 2008
- UPPAAL/DMC – Abstraction-based Heuristics for Directed Model Checking. With Sebastian Kupferschmid, Klaus Dräger, Jörg Hoffmann, Henning Dierks, Andreas Podelski, and Gerd Behrmann. TACAS 2007
- SMT-Based Synthesis of Distributed Systems. With Sven Schewe. AFM 2007
- Distributed Synthesis for Alternating-Time Logics. With Sven Schewe. ATVA 2007
- Slicing Abstractions. With Ingo Brückner, Klaus Dräger, Bernd Finkbeiner, and Heike Wehrheim. Best Paper Award. FSEN 2007
- Bounded Synthesis. With Sven Schewe. ATVA 2007
- Semi-Automatic Distributed Synthesis. With Sven Schewe. JFCS 2007
- Automatic Synthesis of Assumptions for Compositional Model Checking. With Sven Schewe and Matthias Brill. FORTE 2006
- Satisfiability and Finite Model Property for the Alternating-Time µ-Calculus. With Sven Schewe. CSL 2006
- Synthesis of Asynchronous Systems. With Sven Schewe. LOPSTR 2006.
- Directed Model Checking with Distance-Preserving Abstractions. With Klaus Dräger and Andreas Podelski. SPIN 2006
- Semi-Automatic Distributed Synthesis. With Sven Schewe. ATVA 2005
- Uniform Distributed Synthesis. With Sven Schewe. LICS 2005
- LOLA: Runtime Monitoring of Synchronous Systems. With Ben d’Angelo, Sriram Sankaranarayanan, Cesar Sanchez, Will Robinson, Henny B. Sipma, Sandeep Mehrotra, Zohar Manna. TIME 2005
- Collecting Statistics over Runtime Executions. With Sriram Sankaranarayanan and Henny Sipma. FMSD 2005
- Checking Finite Traces using Alternating Automata. With Sriram Sankaranarayanan and Henny Sipma. FMSD 2004
- Collecting Statistics over Runtime Executions. With Henny Sipma. RV 2002
- Using Message Sequence Charts for Component-Based Formal Verification. With Ingolf Krüger. SAVCBS 2001.
- Checking Finite Traces using Alternating Automata. With Henny Sipma. RV 2001
- Language Containment Checking with Nondeterministic BDDs. TACAS 2001
- The `Cash-Point Service: A Verification Case Study Using STeP. With Anca Browne, Zohar Manna and Henny Sipma. FAC 2000.
- Verifying Temporal Properties of Reactive Systems: A STeP Tutorial.
With Nikolaj S. Bjørner, Anca Browne, Michael A. Colón, Zohar Manna, Henny B. Sipma and Tomás E. Uribe. FMSD 2000 - An Update on STeP: Deductive-Algorithmic Verification of Reactive Systems.
With Zohar Manna, Nikolaj S. Bjørner, Anca Browne, Michael A. Colón, Bernd Finkbeiner, Mark Pichora, Henny B. Sipma and Tomás E. Uribe. TOOLS 1999 - Abstraction and Modular Verification of Infinite-State Reactive Systems.
With Zohar Manna, Michael A. Colón, Henny B. Sipma and Tomás E. Uribe. RTSE 1998 - Deductive Verification of Modular Systems. With Zohar Manna and Henny B. Sipma. COMPOS 1997.