Hybride Systeme
2016

[article] bibtexM. Abdelaal, O. E. Theel, C. Kuka, P. Zhang, Y. Gao, V. Bashlovkina, D. Nicklas, und M. Fränzle, "Improving Energy Efficiency in QoSConstrained Wireless Sensor Networks," IJDSN, vol. 2016, p. 1576038:11576038:28, 2016.
@ARTICLE{Abdelaal:Journal16,
author = {Abdelaal, Mohamed and Theel, Oliver E. and Kuka, Christian and Zhang, Peilin and Gao, Yang and Bashlovkina, Vasilisa and Nicklas, Daniela and Fr{\"{a}}nzle, Martin},
title = {Improving Energy Efficiency in {QoS}Constrained Wireless Sensor Networks},
journal = {{IJDSN}},
volume = {2016},
year = {2016},
pages = {1576038:11576038:28},
doi = {10.1155/2016/1576038},
timestamp={Wed, 08 Jun 2016 17:51:00 +0200},
biburl={http://dblp.unitrier.de/rec/bib/journals/ijdsn/AbdelaalTKZGBNF16},
bibsource={dblp computer science bibliography, http://dblp.org},
} 
[techreport] bibtexK. Scheibler, F. Neubauer, A. Mahdi, M. Fränzle, T. Teige, T. Bienmüller, D. Fehrer, und B. Becker, "Extending iSAT3 with ICPContractors for Bitwise Integer Operations," SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 116, 2016.
@TECHREPORT{ATR116,
author = {Scheibler, Karsten and Neubauer, Felix and Mahdi, Ahmed and Fr{\"{a}}nzle, Martin and Teige, Tino and Bienm{\"{u}}ller, Tom and Fehrer, Detlef and Becker, Bernd},
editor = {Becker, Bernd and Damm, Werner and Finkbeiner, Bernd and Fr{\"{a}}nzle, Martin and Olderog, ErnstR{\"{u}}diger and Podelski, Andreas},
title = {Extending {iSAT3} with {ICP}Contractors for Bitwise Integer Operations},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
number = {116},
year = {2016},
institution = {SFB/TR 14 AVACS} } 
[inproceedings] bibtexH. Ody, M. Fränzle, und M. R. Hansen, "Discounted Duration Calculus," in Proc. FM 2016: Formal Methods  21st International Symposium, Limassol, Cyprus, November 911, 2016, Proceedings, 2016, pp. 577592.
@INPROCEEDINGS{FM16DDC,
author = {Ody, Heinrich and Fr{\"{a}}nzle, Martin and Hansen, Michael R.},
editor = {Fitzgerald, John S. and Heitmeyer, Constance L. and Gnesi, Stefania and Philippou, Anna},
title = {Discounted Duration Calculus},
booktitle = {{FM} 2016: Formal Methods  21st International Symposium, Limassol, Cyprus, November 911, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9995},
year = {2016},
pages = {577592} } 
[inproceedings] bibtexM. Chen, M. Fränzle, Y. Li, P. N. Mosaad, und N. Zhan, "Validated SimulationBased Verification of Delayed Differential Dynamics," in Proc. FM 2016: Formal Methods  21st International Symposium, Limassol, Cyprus, November 911, 2016, Proceedings, 2016, pp. 137154.
@INPROCEEDINGS{FM16DDE,
author = {Chen, Mingshuai and Fr{\"{a}}nzle, Martin and Li, Yangjia and Mosaad, Peter Nazier and Zhan, Naijun},
editor = {Fitzgerald, John S. and Heitmeyer, Constance L. and Gnesi, Stefania and Philippou, Anna},
title = {Validated SimulationBased Verification of Delayed Differential Dynamics},
booktitle = {{FM} 2016: Formal Methods  21st International Symposium, Limassol, Cyprus, November 911, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9995},
year = {2016},
pages = {137154} } 
[inproceedings] bibtexK. Scheibler, F. Neubauer, A. Mahdi, M. Fränzle, T. Teige, T. Bienmüller, D. Fehrer, und B. Becker, "Accurate ICPbased FloatingPoint Reasoning," in Proc. Formal Methods in ComputerAided Design (FMCAD 2016), 2016.
@INPROCEEDINGS{FMCAD16,
author = {Scheibler, Karsten and Neubauer, Felix and Mahdi, Ahmed and Fr{\"{a}}nzle, Martin and Teige, Tino and Bienm{\"{u}}ller, Tom and Fehrer, Detlef and Becker, Bernd},
title = {Accurate {ICP}based FloatingPoint Reasoning},
booktitle = {Formal Methods in ComputerAided Design (FMCAD 2016)},
year = {2016},
organization = {FMCAD Inc.},
opteditor={""},
optvolume={""},
optnumber={""},
optseries={""},
optpages={""},
optpublisher={""},
} 
[proceedings] bibtexFORMATS 2016 : 14th International Conference on Formal Modeling and Analysis of Timed Systemsspringer, 2016.
@PROCEEDINGS{FORMATS16, editor = {Fr{\"{a}}nzle, Martin and Markey, Nicolas},
month = aug, title = {FORMATS 2016 : 14th International Conference on Formal Modeling and Analysis of Timed Systems},
series = {lncs},
volume = {9884},
year = {2016},
publisher = {springer} } 
[inproceedings] bibtexA. Mahdi, K. Scheibler, F. Neubauer, M. Fränzle, und B. Becker, "Advancing Software Model Checking Beyond Linear Arithmetic Theories," in Proc. Hardware and Software: Verification and Testing  12th International Haifa Verification Conference, HVC 2016, Haifa, Israel, November 1417, 2016, Proceedings, 2016, pp. 186201.
@INPROCEEDINGS{HVC16,
author = {Mahdi, Ahmed and Scheibler, Karsten and Neubauer, Felix and Fr{\"{a}}nzle, Martin and Becker, Bernd},
title = {Advancing Software Model Checking Beyond Linear Arithmetic Theories},
booktitle = {Hardware and Software: Verification and Testing  12th International Haifa Verification Conference, {HVC} 2016, Haifa, Israel, November 1417, 2016, Proceedings},
year = {2016},
pages = {186201},
doi = {10.1007/9783319490526_12},
crossref = {DBLP:conf/hvc/2016},
timestamp={Wed, 02 Nov 2016 13:49:10 +0100},
biburl={http://dblp.unitrier.de/rec/bib/conf/hvc/MahdiSNFB16},
bibsource={dblp computer science bibliography, http://dblp.org},
} 
[inproceedings] bibtexP. Mosaad, M. Fränzle, und B. Xue, "Temporal Logic Verification for Delay Differential Equations," in Proc. 13th International Colloquium on Theoretical Aspects of Computing, ICTAC 2016, Taipei, Taiwan, ROC, October 2431, 2016, Proceedings, 2016.
@INPROCEEDINGS{ICTAC16,
author = {Mosaad, Peter and Fr{\"{a}}nzle, Martin and Xue, Bai},
editor = {Sampaio, Augusto and Wang, Farn},
title = {Temporal Logic Verification for Delay Differential Equations},
booktitle = {13th International Colloquium on Theoretical Aspects of Computing, {ICTAC} 2016, Taipei, Taiwan, ROC, October 2431, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
year = {2016},
publisher = {Springer},
crossref = {DBLP:conf/ictac/2016} } 
[inproceedings] bibtexS. Khan und M. Fränzle, "Multichannel mode for emergency system in urban connected vehicles," in Proc. 24th IEEE/ACM International Symposium on Quality of Service, IWQoS 2016, Beijing, China, June 2021, 2016, 2016, pp. 12.
@INPROCEEDINGS{iwqos16,
author = {Khan, Saifullah and Fr{\"{a}}nzle, Martin},
title = {Multichannel mode for emergency system in urban connected vehicles},
booktitle = {24th {IEEE/ACM} International Symposium on Quality of Service, IWQoS 2016, Beijing, China, June 2021, 2016},
year = {2016},
pages = {12},
doi = {10.1109/iwqos.2016.7590415},
crossref = {DBLP:conf/iwqos/2016},
timestamp={Wed, 19 Oct 2016 16:43:13 +0200},
biburl={http://dblp.unitrier.de/rec/bib/conf/iwqos/KhanF16},
bibsource={dblp computer science bibliography, http://dblp.org},
} 
[inproceedings] bibtexS. Parisi und A. Lüdtke, "Evaluation of Distributed Situation Awareness on a Ship Bridge," in Proc. Proceedings of the European Conference on Cognitive Ergonomics, New York, NY, USA, 2016, p. 34:134:2.
@INPROCEEDINGS{Parisi:2016:EDS:2970930.2970965,
author = {Parisi, Stella and L{\"{u}}dtke, Andreas},
keywords = {Distributed Situation Awareness, Fuzzy Cognitive Maps, Human Factors, Situation Awareness, User Interfaces},
title = {Evaluation of Distributed Situation Awareness on a Ship Bridge},
booktitle = {Proceedings of the European Conference on Cognitive Ergonomics},
series = {ECCE '16},
year = {2016},
pages = {34:134:2},
publisher = {ACM},
location = {Nottingham, United Kingdom},
address = {New York, NY, USA},
isbn = {9781450342445},
doi = {10.1145/2970930.2970965},
articleno={34},
numpages={2},
acmid={2970965},
} 
[proceedings] bibtexDependable Software Engineering: Theories, Tools, and Applications  Second International Symposium, SETTA 2016, Beijing, China, November 911, 2016, Proceedings, 2016.
@PROCEEDINGS{SETTA16, editor = {Fr{\"{a}}nzle, Martin and Kapur, Deepak and Zhan, Naijun},
title = {Dependable Software Engineering: Theories, Tools, and Applications  Second International Symposium, {SETTA} 2016, Beijing, China, November 911, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9984},
year = {2016},
isbn = {9783319476766},
doi = {10.1007/9783319476773},
timestamp={Thu, 20 Oct 2016 14:55:50 +0200},
biburl={http://dblp.unitrier.de/rec/bib/conf/setta/2016},
bibsource={dblp computer science bibliography, http://dblp.org},
} 
[inproceedings] bibtexY. Gao und M. Fränzle, "CSiSAT: A Satisfiability Solver for SMT Formulas with Continuous Probability Distributions," in Proc. SNR 2016: 2nd International Workshop on Symbolic and Numerical Methods for Reachability Analysis, 2016.
@INPROCEEDINGS{SNR16,
author = {Gao, Yang and Fr{\"{a}}nzle, Martin},
editor = {{\'{A}}brah{\'{a}}m, Erika and Bogomolov, Sergiy},
title = {{CSiSAT}: A Satisfiability Solver for {SMT} Formulas with Continuous Probability Distributions},
booktitle = {SNR 2016: 2nd International Workshop on Symbolic and Numerical Methods for Reachability Analysis},
year = {2016},
organization = {IEEE},
optvolume={""},
optnumber={""},
optseries={""},
optpages={""},
optpublisher={""},
} 
[proceedings] bibtexHardware and Software: Verification and Testing  12th International Haifa Verification Conference, HVC 2016, Haifa, Israel, November 1417, 2016, Proceedings, 2016.
@PROCEEDINGS{DBLP:conf/hvc/2016, editor = {Bloem, Roderick and Arbel, Eli},
title = {Hardware and Software: Verification and Testing  12th International Haifa Verification Conference, {HVC} 2016, Haifa, Israel, November 1417, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10028},
year = {2016},
isbn = {9783319490519},
doi = {10.1007/9783319490526},
timestamp={Wed, 02 Nov 2016 13:48:29 +0100},
biburl={http://dblp.unitrier.de/rec/bib/conf/hvc/2016},
bibsource={dblp computer science bibliography, http://dblp.org},
} 
[proceedings] bibtexTheoretical Aspects of Computing  ICTAC 2016  13th International Colloquium, Taipei, Taiwan, ROC, October 2431, 2016, Proceedings, 2016.
@PROCEEDINGS{DBLP:conf/ictac/2016, editor = {Sampaio, Augusto and Wang, Farn},
title = {Theoretical Aspects of Computing  {ICTAC} 2016  13th International Colloquium, Taipei, Taiwan, ROC, October 2431, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9965},
year = {2016},
isbn = {9783319467498},
doi = {10.1007/9783319467504},
timestamp={Mon, 17 Oct 2016 16:33:42 +0200},
biburl={http://dblp.unitrier.de/rec/bib/conf/ictac/2016},
bibsource={dblp computer science bibliography, http://dblp.org},
} 
[proceedings] bibtex  Dokument aufrufen24th IEEE/ACM International Symposium on Quality of Service, IWQoS 2016, Beijing, China, June 2021, 2016IEEE, 2016.
@PROCEEDINGS{DBLP:conf/iwqos/2016, title = {24th {IEEE/ACM} International Symposium on Quality of Service, IWQoS 2016, Beijing, China, June 2021, 2016},
year = {2016},
publisher = {IEEE},
isbn = {9781509026340},
url = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=7584862},
timestamp={Wed, 19 Oct 2016 16:42:42 +0200},
biburl={http://dblp.unitrier.de/rec/bib/conf/iwqos/2016},
bibsource={dblp computer science bibliography, http://dblp.org},
}
2015

[article] bibtexY. Gao und M. Fränzle, "Verification of Stochastic Systems by Stochastic Satisfiability Modulo Theories with Continuous Domain," Symbolic and Numerical Methods for Reachability Analysis, 1st International Workshop, SNR 2015, vol. 37, pp. 210, 2015.
@ARTICLE{,
author = {Gao, Yang and Fr{\"{a}}nzle, Martin},
editor = {Bogomolov, Sergiy and Tiwari, Ashish},
title = {Verification of Stochastic Systems by Stochastic Satisfiability Modulo Theories with Continuous Domain},
journal = {Symbolic and Numerical Methods for Reachability Analysis, 1st International Workshop, SNR 2015},
volume = {37},
year = {2015},
pages = {210},
issn = {2040557X},
abstract = {Stochastic Satisfiability Modulo Theories (SSMT) is a quantitative exten sion of classical Satisfiability Modulo Theories (SMT) inspired by stochastic logics. It extends SMT by the usual as well as randomized quantifiers, fa cilitating capture of stochastic game properties in the logic, like reachability analysis of hybridstate Markov decision processes. Solving for SSMT for mulae with quantification over finite and thus discrete domain has been ad dressed by Tino Teige et al. In our work, we extend their work to SSMT over continuous quantifier domains (CSSMT) in order to enable capture of, e.g., continuous disturbances and uncertainty in hybrid systems. We extend the semantics of SSMT and introduce a corresponding solving procedure. A discussion regarding to reachability analysis is given to demonstrate applica bility of our framework to reachability problems in hybrid systems.} } 
[inproceedings] bibtexM. Amri, Y. Becis, D. Aubry, N. Ramdani, und M. Fränzle, "Robust indoor location tracking of multiple inhabitants using only binary sensors," in Proc. IEEE International Conference on Automation Science and Engineering, CASE 2015, Gothenburg, Sweden, August 2428, 2015, 2015, pp. 194199.
@INPROCEEDINGS{Amrietal:CASE15,
author = {Amri, Mohamed{}Hedi and Becis, Yasmina and Aubry, Didier and Ramdani, Nacim and Fr{\"{a}}nzle, Martin},
title = {Robust indoor location tracking of multiple inhabitants using only binary sensors},
booktitle = {{IEEE} International Conference on Automation Science and Engineering, {CASE} 2015, Gothenburg, Sweden, August 2428, 2015},
year = {2015},
pages = {194199},
publisher = {{IEEE}},
doi = {10.1109/coase.2015.7294061},
timestamp={Tue, 13 Oct 2015 09:07:07 +0200},
biburl={http://dblp.unitrier.de/rec/bib/conf/case/AmriBARF15},
bibsource={dblp computer science bibliography, http://dblp.org},
} 
[article] bibtexA. Eggers, N. Ramdani, N. S. Nedialkov, und M. Fränzle, "Improving the SAT Modulo ODE Approach to Hybrid Systems Analysis by Combining Different Enclosure Methods," Softw. Syst. Model., vol. 14, iss. 1, pp. 121148, 2015.
@ARTICLE{Eggers:2015:ISM:2733585.2733610,
author = {Eggers, Andreas and Ramdani, Nacim and Nedialkov, Nedialko S. and Fr{\"{a}}nzle, Martin},
keywords = {Analysis of hybrid discretecontinuous systems, bracketing systems, Enclosure methods for ODEs, satisfiability modulo theories},
month = feb, title = {Improving the SAT Modulo ODE Approach to Hybrid Systems Analysis by Combining Different Enclosure Methods},
journal = {Softw. Syst. Model.},
volume = {14},
number = {1},
year = {2015},
pages = {121148},
publisher = {SpringerVerlag New York, Inc.},
address = {Secaucus, NJ, USA},
issn = {16191366},
doi = {10.1007/s1027001202953},
issue_date={February 2015},
numpages={28},
acmid={2733610},
} 
[inproceedings] bibtexY. Page, F. Fahrenkrog, A. Fiorentino, M. Fränzle, J. Gwehenberger, T. Helmer, M. Lindman, O. op den Camp, S. Puch, L. van Rooi, U. Sander, und P. Wimmer, "A Comprehensive and Harmonized Method for Assessing the Effectiveness of Advanced Driver Assistance Systems by Virtual Simulation: The P.E.A.R.S. Initiative," in Proc. The 24th International Technical Conference on the Enhanced Safety of Vehicles (ESV), Gothenburg, Sweden, 2015.
@INPROCEEDINGS{esv2015,
author = {Page, Yves and Fahrenkrog, Felix and Fiorentino, Anita and Fr{\"{a}}nzle, Martin and Gwehenberger, Johann and Helmer, Thomas and Lindman, Magdalena and op den Camp, Olaf and Puch, Stefan and van Rooi, Lex and Sander, Ulrich and Wimmer, Peter},
month = {June},
title = {{A Comprehensive and Harmonized Method for Assessing the Effectiveness of Advanced Driver Assistance Systems by Virtual Simulation: The P.E.A.R.S. Initiative}},
booktitle = {The 24th International Technical Conference on the Enhanced Safety of Vehicles (ESV)},
year = {2015},
organization = {National Highway Traffic Safety Administration},
address = {Gothenburg, Sweden},
note = {PAPERNO.150370} } 
[article] bibtexM. Fakih, K. Grüttner, M. Fränzle, und A. Rettberg, "Statebased realtime analysis of SDF applications on MPSoCs with shared communication resources," Journal of Systems Architecture  Embedded Systems Design, vol. 61, iss. 9, pp. 486509, 2015.
@ARTICLE{Fakih:JSA15,
author = {Fakih, Maher and Gr{\"{u}}ttner, Kim and Fr{\"{a}}nzle, Martin and Rettberg, Achim},
title = {Statebased realtime analysis of {SDF} applications on MPSoCs with shared communication resources},
journal = {Journal of Systems Architecture  Embedded Systems Design},
volume = {61},
number = {9},
year = {2015},
pages = {486509},
doi = {10.1016/j.sysarc.2015.04.005},
timestamp={Thu, 26 Nov 2015 09:26:36 +0100},
biburl={http://dblp.unitrier.de/rec/bib/journals/jsa/FakihGFR15},
bibsource={dblp computer science bibliography, http://dblp.org},
} 
[incollection] bibtexM. Fränzle, S. Gerwinn, P. Kröger, A. Abate, und J. Katoen, "Multiobjective Parameter Synthesis in Probabilistic Hybrid Systems," in Formal Modeling and Analysis of Timed Systems, Sankaranarayanan, S. und Vicario, E., Eds., Springer International Publishing, 2015, vol. 9268, pp. 93107.
@INCOLLECTION{FraenzleEtAL2015,
author = {Fr{\"{a}}nzle, Martin and Gerwinn, Sebastian and Kr{\"{o}}ger, Paul and Abate, Alessandro and Katoen, JoostPieter},
editor = {Sankaranarayanan, Sriram and Vicario, Enrico},
title = {Multiobjective Parameter Synthesis in Probabilistic Hybrid Systems},
booktitle = {Formal Modeling and Analysis of Timed Systems},
series = {Lecture Notes in Computer Science},
volume = {9268},
year = {2015},
pages = {93107},
publisher = {Springer International Publishing},
isbn = {9783319229744},
doi = {10.1007/9783319229751_7},
language={English},
} 
[article] bibtexY. Gao und M. Fränzle, "A Solving Procedure for Stochastic Satisfiability Modulo Theories with Continuous Domain," Quantitative Evaluation of Systems, vol. 9259, pp. 295311, 2015.
@ARTICLE{gao2015solving,
author = {Gao, Yang and Fr{\"{a}}nzle, Martin},
title = {A Solving Procedure for Stochastic Satisfiability Modulo Theories with Continuous Domain},
journal = {Quantitative Evaluation of Systems},
volume = {9259},
year = {2015},
pages = {295311} } 
[inproceedings] bibtexL. Zou, N. Zhan, S. Wang, und M. Fränzle, "Formal Verification of Simulink/Stateflow Diagrams," in Proc. Automated Technology for Verification and Analysis  13th International Symposium, ATVA 2015, Shanghai, China, October 1215, 2015, Proceedings, 2015, pp. 464481.
@INPROCEEDINGS{Liang:ATVA15,
author = {Zou, Liang and Zhan, Naijun and Wang, Shuling and Fr{\"{a}}nzle, Martin},
editor = {Finkbeiner, Bernd and Pu, Geguang and Zhang, Lijun},
title = {Formal Verification of Simulink/Stateflow Diagrams},
booktitle = {Automated Technology for Verification and Analysis  13th International Symposium, {ATVA} 2015, Shanghai, China, October 1215, 2015, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9364},
year = {2015},
pages = {464481},
publisher = {Springer},
doi = {10.1007/9783319249537_33},
timestamp={Thu, 08 Oct 2015 12:37:28 +0200},
biburl={http://dblp.unitrier.de/rec/bib/conf/atva/ZouZWF15},
bibsource={dblp computer science bibliography, http://dblp.org},
} 
[inproceedings] bibtexL. Zou, M. Fränzle, N. Zhan, und P. N. Mosaad, "Automatic Verification of Stability and Safety for Delay Differential Equations," in Proc. Computer Aided Verification  27th International Conference, CAV 2015, San Francisco, CA, USA, July 1824, 2015, Proceedings, Part II, 2015, pp. 338355.
@INPROCEEDINGS{MF:CAV15DDE,
author = {Zou, Liang and Fr{\"{a}}nzle, Martin and Zhan, Naijun and Mosaad, Peter Nazier},
title = {Automatic Verification of Stability and Safety for Delay Differential Equations},
booktitle = {Computer Aided Verification  27th International Conference, {CAV} 2015, San Francisco, CA, USA, July 1824, 2015, Proceedings, Part {II}},
year = {2015},
pages = {338355},
doi = {10.1007/9783319216683_20},
crossref = {DBLP:conf/cav/2015},
timestamp={Mon, 20 Jul 2015 11:19:16 +0200},
biburl={http://dblp.unitrier.de/rec/bib/conf/cav/ZouFZM15},
bibsource={dblp computer science bibliography, http://dblp.org},
} 
[inproceedings] bibtexM. Fränzle, M. R. Hansen, und H. Ody, "No Need Knowing Numerous Neighbours  Towards a Realizable Interpretation of MLSL," in Proc. Correct System Design  Symposium in Honor of ErnstRüdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 89, 2015. Proceedings, 2015, pp. 152171.
@INPROCEEDINGS{MFetal:ERO60,
author = {Fr{\"{a}}nzle, Martin and Hansen, Michael R. and Ody, Heinrich},
editor = {Meyer, Roland and Platzer, Andr{\'{e}} and Wehrheim, Heike},
title = {No Need Knowing Numerous Neighbours  Towards a Realizable Interpretation of {MLSL}},
booktitle = {Correct System Design  Symposium in Honor of ErnstR{\"{u}}diger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 89, 2015. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9360},
year = {2015},
pages = {152171},
publisher = {Springer},
doi = {10.1007/9783319235066_11},
timestamp={Fri, 04 Sep 2015 13:09:10 +0200},
biburl={http://dblp.unitrier.de/rec/bib/conf/birthday/FranzleHO15},
bibsource={dblp computer science bibliography, http://dblp.org},
} 
[inproceedings] bibtexN. Müllner, M. Fränzle, und S. Fröschle, "Estimating the Probability of a Timely TrafficHazard Warning via Simulation," in Proc. Proceedings of the 48th Annual Symposium on Simulation (AnSS2015), Washington DC, USA, 2015.
@INPROCEEDINGS{Muellner:SpringSim2015,
author = {M{\"{u}}llner, Nils and Fr{\"{a}}nzle, Martin and Fr{\"{o}}schle, Sibylle},
month = {April},
title = {Estimating the Probability of a Timely TrafficHazard Warning via Simulation},
booktitle = {Proceedings of the 48th Annual Symposium on Simulation (AnSS2015)},
year = {2015},
publisher = {IEEE Computer Society Press},
address = {Washington DC, USA},
abstract = {Traffic flow simulation is exploited for estimating the probability that a message \, a hazard warning in this case \, is correctly transmitted to an approaching car in time, that is, before overstepping a safety threshold. The results derived by simulation provide valuable insights in the functional relation between the numerous authoritative parameters and the reliability of timely message reception.},
access={restricted},
bibtex={muellner.anss.2015.bib},
category={Automatic Verification},
conferencelong={Symposium on Simulation},
conferenceshort={ANSS},
crosssite={""},
pdf={muellner.anss.2015.pdf},
subproject={H1/2},
} 
[article] bibtex  Dokument aufrufenE. Olderog und M. Swaminathan, "Structural Transformations for DataEnriched RealTime Systems," Formal Aspects of Computing, vol. 27, iss. 4, pp. 727750, 2015.
@ARTICLE{OlderogSwami2015,
author = {Olderog, ErnstR{\"{u}}diger and Swaminathan, Mani},
keywords = {Communication Closedness, Extended Timed Automata, Flattening, Layered Composition, Layered reachability, Noninterference and Precedence, Realtime Mutual Exclusion, Separation, Structural transformations},
month = aug, title = {Structural Transformations for DataEnriched RealTime Systems},
journal = {Formal Aspects of Computing},
volume = {27},
number = {4},
year = {2015},
pages = {727750},
url = {http://dx.doi.org/10.1007/s001650140306y},
doi = {10.1007/s001650140306y},
abstract = {We investigate designlevel structural transformations that aim at easier subsequent verification of realtime systems with shared data variables, modelled as networks of extended timed automata (ETA). Our contributions to this end are the following: (1) We first equip ETA with an operator for layered composition, intermediate between parallel and sequential composition. Under certain noninterference and / or precedence conditions imposed on the structure of the ETA networks, the Communication Closed Layer (CCL) laws and associated partialorder (po) and (layered) reachability equivalences are shown to hold. (2) Next, we investigate (under certain cycle conditions on the ETA) the (reachability preserving) transformations of separation and flattening aimed at reducing the number of cycles of the ETA. (3) We then show that our separation and flattening in (2) may be applied together with the CCL laws in (1), in order to restructure ETA networks such that the verification of layered reachability properties is rendered easier. This interplay of the three structural transformations (separation, flattening, and layering) is demonstrated on an enhanced version of Fischer’s realtime mutual exclusion protocol for access to multiple critical sections.} } 
[inproceedings] bibtex  Dokument aufrufenS. Khan und M. Fränzle, "Robust midrange communication in urban VANETs." 2015, pp. 115120.
@INPROCEEDINGS{SKhanEtAL20151,
author = {Khan, S. and Fr{\"{a}}nzle, Martin},
keywords = {Robust communication, routing protocols, Trafﬁc awareness, Vehicular adhoc networks (VANETs)},
month = jul, title = {Robust midrange communication in urban VANETs},
year = {2015},
pages = {115120},
publisher = {IEEE},
location = {South Korea},
organization = {ICACT},
isbn = {9788996865049},
url = {http://ieeexplore.ieee.org/xpl/articleDetails.jsp?reload=true&arnumber=7224769&punumber%3D7166144%26filter%3DAND%28p_IS_Number%3A7224736%29%26pageNumber%3D2},
doi = {10.1109/ICACT.2015.7224769},
abstract = {Cooperative driving and the associated need for vehicular communication motivate vehicular adhoc networks (VANETs). One major challenge is to provide for robust communication  in spite of highly dynamic topologies and the presence of shielding obstacles  without installing extra relay infrastructure. Trafficdensity information and density estimation schemes are a valuable asset to approach this challenge. In this light we propose a novel routing protocol. Furthermore, extensive simulations are provided to support our case.} } 
[inproceedings] bibtexS. Khan, M. Alam, N. Mullner, und M. Franzle, "Cooperation and network coding based MAC protocol for VANETs," in Proc. Vehicular Networking Conference (VNC), 2015 IEEE, 2015, pp. 6467.
@INPROCEEDINGS{SKhanEtAL20152,
author = {Khan, S. and Alam, M. and Mullner, N. and Franzle, M.},
keywords = {access protocols, ARQMAC, automatic repeat request, CNCMAC protocol, cooperative ARQMAC, cooperative automatic repeat request, cooperative communication, cooperative communications, Media Access Protocol, network coding, network coding based MAC protocol, network coding techniques, relay nodes, Relays, Signal to noise ratio, Throughput, VANET, vehicular ad hoc networks, Vehicular Adhoc Networks},
month = {Dec},
title = {Cooperation and network coding based MAC protocol for VANETs},
booktitle = {Vehicular Networking Conference (VNC), 2015 IEEE},
year = {2015},
pages = {6467},
doi = {10.1109/vnc.2015.7385548} }
2014

[inproceedings] bibtexN. Müllner, O. Theel, und M. Fränzle, "Composing Thermostatically Controlled Loads to Determine the Reliability against Blackouts," in Proc. Proceedings of the 10th International Symposium on Frontiers of Information Systems and Network Applications (FINA2014), 2014, pp. 334341.
@INPROCEEDINGS{,
author = {M{\"{u}}llner, Nils and Theel, Oliver and Fr{\"{a}}nzle, Martin},
month = may, title = {Composing Thermostatically Controlled Loads to Determine the Reliability against Blackouts},
booktitle = {Proceedings of the 10th International Symposium on Frontiers of Information Systems and Network Applications (FINA2014)},
year = {2014},
pages = {334341},
location = {Victoria, BC, Canada} } 
[inproceedings] bibtexN. Müllner, O. Theel, und M. Fränzle, "Combining Decomposition and Lumping to Evaluate Semihierarchical Systems," in Proc. Proceedings of the 28th IEEE International Conference on Advanced Information Networking and Applications (AINA2014), 2014, pp. 10491056.
@INPROCEEDINGS{,
author = {M{\"{u}}llner, Nils and Theel, Oliver and Fr{\"{a}}nzle, Martin},
month = may, title = {Combining Decomposition and Lumping to Evaluate Semihierarchical Systems},
booktitle = {Proceedings of the 28th IEEE International Conference on Advanced Information Networking and Applications (AINA2014)},
year = {2014},
pages = {10491056},
location = {Victoria, BC, Canada} } 
[phdthesis] bibtex  Dokument aufrufenN. Müllner, "Unmasking fault tolerance: Quantifying deterministic recovery dynamics in probabilistic environments," PhD Thesis , 2014.
@PHDTHESIS{,
author = {M{\"{u}}llner, Nils},
month = feb, title = {Unmasking fault tolerance: Quantifying deterministic recovery dynamics in probabilistic environments},
year = {2014},
school = {Carl von Ossietzky Universit{\"{a}}t Oldenburg},
note = {175 pages of contents and appendix of 188 overall pages},
url = {http://www.unioldenburg.de/fileadmin/user_upload/informatik/Mue14.pdf} } 
[inproceedings] bibtexA. Mahdi und M. Fränzle, "Generalized Craig Interpolation for Stochastic Satisfiability Modulo Theory Problems," in Proc. Reachability Problems  8th International Workshop, RP 2014, Oxford, UK, September 2224, 2014. Proceedings, 2014, pp. 203215.
@INPROCEEDINGS{DBLP:conf/rp/MahdiF14,
author = {Mahdi, Ahmed and Fr{\"{a}}nzle, Martin},
title = {Generalized Craig Interpolation for Stochastic Satisfiability Modulo Theory Problems},
booktitle = {Reachability Problems  8th International Workshop, {RP} 2014, Oxford, UK, September 2224, 2014. Proceedings},
year = {2014},
pages = {203215},
doi = {10.1007/9783319114392_16},
crossref = {DBLP:conf/rp/2014},
timestamp={Wed, 08 Oct 2014 12:10:38 +0200},
biburl={http://dblp.unitrier.de/rec/bib/conf/rp/MahdiF14},
bibsource={dblp computer science bibliography, http://dblp.org},
} 
[inproceedings] bibtexA. Mahdi, B. Westphal, und M. Fränzle, "Transformations for Compositional Verification of AssumptionCommitment Properties," in Proc. Reachability Problems  8th International Workshop, RP 2014, Oxford, UK, September 2224, 2014. Proceedings, 2014, pp. 216229.
@INPROCEEDINGS{DBLP:conf/rp/MahdiWF14,
author = {Mahdi, Ahmed and Westphal, Bernd and Fr{\"{a}}nzle, Martin},
title = {Transformations for Compositional Verification of AssumptionCommitment Properties},
booktitle = {Reachability Problems  8th International Workshop, {RP} 2014, Oxford, UK, September 2224, 2014. Proceedings},
year = {2014},
pages = {216229},
doi = {10.1007/9783319114392_17},
crossref = {DBLP:conf/rp/2014},
timestamp={Wed, 08 Oct 2014 12:13:48 +0200},
biburl={http://dblp.unitrier.de/rec/bib/conf/rp/MahdiWF14},
bibsource={dblp computer science bibliography, http://dblp.org},
} 
[phdthesis] bibtex  Dokument aufrufenA. Eggers, "Direct Handling of Ordinary Differential Equations in ConstraintSolvingBased Analysis of Hybrid Systems," PhD Thesis , Germany, 2014.
@PHDTHESIS{eggers:phd:2014,
author = {Eggers, Andreas},
title = {Direct Handling of Ordinary Differential Equations in ConstraintSolvingBased Analysis of Hybrid Systems},
type = {Doctoral Dissertation},
year = {2014},
school = {Carl von Ossietzky Universit{\"{a}}t Oldenburg, Fakult{\"{a}}t II, Department of Computing Science},
address = {Germany},
note = {Referees: Martin Fr{\"{a}}nzle and Nacim Ramdani, open access: \url{http://oops.unioldenburg.de/id/eprint/1911}},
url = {http://oops.unioldenburg.de/id/eprint/1911},
abstract = {In this thesis, the behavior of hybrid discretecontinuous systems is analyzed using a Bounded Model Checking (BMC) approach, i.e. by finitely unwinding the systems' transition relations as formulae. Contrary to earlier BMC approaches for hybrid systems, we allow Ordinary Differential Equations (ODEs) directly in the formula, introducing the problem class of Satisfiability (SAT) modulo ODE. The main contribution of the thesis and its underlying publications is the direct handling of SAT modulo ODE formulae by combining the iSAT solver for boolean combinations of nonlinear arithmetic constraints with the VNODELP library for computing validated numerical enclosures for ODE solutions. This iSATODE solver comprises several algorithmic enhancements, like caching of intermediate results and previous queries, bracketing systems, and the deduction of trajectory directions, all of which are subjected to evaluation on academic case studies and compared with results from the literature.},
access={open},
subproject={h12},
bibtex={eggers.phd.2014.bib},
pdf={eggers.phd.2014.pdf},
} 
[article] bibtexC. Ellen, S. Gerwinn, und M. Fränzle, "Statistical model checking for stochastic hybrid systems involving nondeterminism over continuous domains," International Journal on Software Tools for Technology Transfer, pp. 120, 2014.
@ARTICLE{Ellen2014statistical,
author = {Ellen, Christian and Gerwinn, Sebastian and Fr{\"{a}}nzle, Martin},
keywords = {Nondeterminism, SSMT, Statistical model checking, Stochastic hybrid systems},
title = {Statistical model checking for stochastic hybrid systems involving nondeterminism over continuous domains},
journal = {International Journal on Software Tools for Technology Transfer},
year = {2014},
pages = {120},
publisher = {Springer Berlin Heidelberg},
issn = {14332779},
doi = {10.1007/s100090140329y},
abstract = {Behavioral veriﬁcation of technical systems involving both discrete and continuous components is a common and demanding task. The behavior of such systems can often be characterized using stochastic hybrid automata, leading to veriﬁcation problems which can be formalized and solved using stochastic logic calculi like Stochastic Satisﬁability Modulo Theory (SSMT). While algorithms for discharging proof obligations in SSMT form exist, their applicability is limited due to the computational complexity, which often increases exponentially with the number of quantiﬁed variables. Recently, statistical model checking has been successfully applied to stochastic hybrid systems, thereby increasing the size of the system for which veriﬁcation problems is tractable. However, being based on randomized simulation, these methods usually cannot handle nondeterminism. In previous work, we have deviated from the usual approach of simulating the model and rather proposed a statistical method for SSMT solving which, being based on statistical AI planning algorithms, can also treat nondeterminism over a ﬁnite domain. Here, we extend this previous work to the case of continuous domains. In particular, using ideas from noisy optimization, we adaptively build up a decision tree recording the ﬁndings and guiding further exploration, thereby favoring the currently most promising subdomain. The nondeterminism is resolved by translating the satisfaction problem into an optimization problem, thereby computing both optimistic and pessimistic bounds on the probability of satisfaction. At each stage of the evaluation process, we show how to obtain conﬁdence statements about the probability of satisfaction for the overall SSMT formula, including reliable estimates on the optimal resolution of any nondeterministic choice involved.},
language={English},
owner={cellen},
timestamp={2014.08.06},
} 
[inproceedings] bibtexM. Fakih, K. Grüttner, M. Fränzle, und A. Rettberg, "Mulitcore Performance Analysis of a MultiPhase Electrical Motor Controller," in Proc. Proceedings of the Embedded Real Time Software and Systems Congress (ERTS$^2$), 2014.
@INPROCEEDINGS{ERTSS14,
author = {Fakih, Maher and Gr{\"{u}}ttner, Kim and Fr{\"{a}}nzle, Martin and Rettberg, Achim},
month = feb, title = {Mulitcore Performance Analysis of a MultiPhase Electrical Motor Controller},
booktitle = {Proceedings of the Embedded Real Time Software and Systems Congress (ERTS$^2$)},
year = {2014},
note = {With 10 pages},
abstract = {The timing predictability of embedded systems with hard realtime requirements is fundamental for guaranteeing their safe usage. With the emergence of multicore platforms this task becomes even more challenging, because of shared processing, communication and memory resources. In this paper, a combination of simulative method with a performance analysis based on modelchecking is proposed. The simulative approach is used for functional validation of the Synchronous Data Flow Application (SDFA) implementation and its mapping on the targeted hardware platform. In our proposed methodology, we are using a binarycompatible and cycleaccurate virtual platform representation to simulate and map all relevant architectural properties to our analytical performance model. In combination, the modelchecking based method allows to guarantee timing bounds of multiple Synchronous Data Flow Application (SDFA) implementations. This approach utilizes Timed Automata (TA) as a common semantic model to represent WCET of software components (SDF actors) and access protocols including timing of shared buses, shared DMAs, private local and shared memories of the multicore platform. The resulting network of TA is analyzed using the UPPAAL modelchecker for providing safe timing bounds of the implementation. We demonstrate our approach using a multiphase electric motor control algorithm (modeled as SDFA) mapped to Infineon's TriCorebased Aurix multicore hardware platform.} } 
[proceedings] bibtexHSCC '14: Proceedings of the 17th International Conference on Hybrid Systems: Computation and ControlNew York, NY, USA: ACM, 2014.
@PROCEEDINGS{Fraanzle:2014:2562059, editor = {Fr{\"{a}}nzle, Martin and Lygeros, John},
month = apr, title = {HSCC '14: Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control},
year = {2014},
publisher = {ACM},
location = {Berlin, Germany},
address = {New York, NY, USA},
note = {100141},
isbn = {9781450327329} } 
[inproceedings] bibtexM. Abdelaal, Y. Gao, M. Fränzle, und O. Theel, "EAVS: Energy Aware Virtual Sensing for Wireless Sensor Networks," in Proc. ISSNIP 2014  Symposium on Sensor Networks, 2014, pp. 16.
@INPROCEEDINGS{ISSNIP14,
author = {Abdelaal, Mohamed and Gao, Yang and Fr{\"{a}}nzle, Martin and Theel, Oliver},
title = {EAVS: Energy Aware Virtual Sensing for Wireless Sensor Networks},
booktitle = {ISSNIP 2014  Symposium on Sensor Networks},
year = {2014},
pages = {16},
organization = {IEEE} } 
[book] bibtexN. Müllner, Unmasking fault tolerance: Quantifying deterministic recovery dynamics in probabilistic environments, Ammerländer Heerstr. 114118, 26111 Oldenburg: BISVerlag der Carl von Ossietzky Universität Oldenburg, 2014.
@BOOK{Muellner2014c,
author = {M{\"{u}}llner, Nils},
month = {February},
title = {Unmasking fault tolerance: Quantifying deterministic recovery dynamics in probabilistic environments},
year = {2014},
pages = {i  xiv, 1166},
publisher = {BISVerlag der Carl von Ossietzky Universit{\"{a}}t Oldenburg},
school = {Carl von Ossietzky Universit{\"{a}}t Oldenburg},
address = {Ammerl\"ander Heerstr. 114118, 26111 Oldenburg},
note = {The book is the revised version of a PhD thesis with the same title.},
isbn = {9783814223193},
abstract = {The present book focuses on distributed systems operating under probabilistic influences like faults. How well can such systems provide their service under the effects of faults? How well can they recover from faults? Along with a thorough introduction into the area of fault tolerance, this book introduces a measure called \emph{limiting window availability} to answer such questions. Furthermore, a method for computing the limiting window availability based on constructing the transition models from the system and environment models is developed. The method yet hinges on the transition model being exponential in the size of the constituting system models. This effect is commonly known as \emph{state space explosion}. Combining \emph{decomposition} and \emph{lumping} \, methods for reducing the state space from the domain of model checking \, yet allows to dampen the state space explosion, thus enhancing the spectrum of systems that are tractable for an analysis significantly.},
numpages={180},
} 
[inproceedings] bibtexM. Oertel, A. Mahdi, E. Böde, und A. Rettberg, "Contractbased Safety: Specification and Application Guidelines," in Proc. Proceedings of the 1st International Workshop on Emerging Ideas and Trends in Engineering of CyberPhysical Systems (EITEC 2014), 2014.
@INPROCEEDINGS{oertel2014,
author = {Oertel, Markus and Mahdi, Ahmed and B{\"{o}}de, Eckard and Rettberg, Achim},
title = {Contractbased Safety: Specification and Application Guidelines},
booktitle = {Proceedings of the 1st International Workshop on Emerging Ideas and Trends in Engineering of CyberPhysical Systems (EITEC 2014)},
year = {2014},
publisher = {Springer},
note = {Research related to qualification and certification of safety properties is mainly driven by two objectives, that are currently being addressed independently: the creation of reusable and modular safety cases as well as the direct integration of safety properties in the model based development artifacts abandoning separate analysis models. In this paper, we present a contract based specification approach allowing to reason about fault containment properties of components in a modular, reusable way. We link formalized safety requirements to typical development models like EASTADL, Simulink and AUTOSAR to state the needed properties and relations enabling analyzability of systems without any changes in industrial format, toolchains and processes. The identification of the necessary safety artifacts to express safety concepts has been performed based on the ISO 26262, but can be applied also to other safety standards. Furthermore, we provide stepbystep application guidelines for the specification of safety concepts that can also be applied by engineers without a background in formal methods. The specification covers all typical areas of safety concepts like definitions of faults/failures, fault containment, expression of safety mechanisms or handling of degradation modes and safe states at multiple abstraction levels. Although the main focus is on the specification, we shortly introduce the possible analysis targets and clarify the interface between the safety view and the functional design. Finally, the approach is applied to a case study.} }
2013

[article] bibtex  Dokument aufrufenN. Müllner, O. Theel, und M. Fränzle, "Combining Decomposition and Reduction for the State Space Analysis of SelfStabilizing Systems," Journal of Computer and System Sciences (JCSS), vol. 79, iss. 7, pp. 11131125, 2013.
@ARTICLE{Muellner2013,
author = {M{\"{u}}llner, Nils and Theel, Oliver and Fr{\"{a}}nzle, Martin},
keywords = {fault tolerance, Limiting window availability, Markov chains, Probabilistic bisimilarity, Probabilistic model checking, Self stabilization},
key = {Muellner2013},
month = nov, title = {Combining Decomposition and Reduction for the State Space Analysis of SelfStabilizing Systems},
journal = {Journal of Computer and System Sciences (JCSS)},
volume = {79},
number = {7},
year = {2013},
pages = {11131125},
issn = {00220000},
url = {http://www.sciencedirect.com/science/article/pii/S0022000013000329},
doi = {10.1016/j.jcss.2013.01.022},
abstract = {Fault tolerance measures of distributed systems can be calculated precisely by state space analysis of the Markov chain corresponding to the product of the system components. The power of such an approach is inherently confined by the state space explosion, i.e. the exponential growth of the Markov chain in the size of the underlying system. We propose a decompositional method to alleviate this limitation. Lumping is a wellknown reduction technique facilitating computation of the relevant measures on the quotient of the Markov chain under lumping equivalence. In order to avoid computation of lumping equivalences on intractably large Markov chains, we propose a system decomposition supporting local lumping on the considerably smaller Markov chains of the subsystems. Recomposing the lumped Markov chains of the subsystems constructs a lumped transition model of the whole system, thus avoiding the construction of the full product chain. An example demonstrates how the limiting window availability (i.e. a particular fault tolerance measure) can be computed for a selfstabilizing system exploiting lumping and decomposition.} } 
[incollection] bibtex  Dokument aufrufenS. Puch, B. Wortelen, M. Fränzle, und T. Peikenkamp, "Evaluation of Drivers Interaction with Assistant Systems using Criticality Driven Guided Simulation," in Digital Human Modeling and Applications in Health, Safety, Ergonomics, and Risk Management. Healthcare and Safety of the Environment and Transport, Duffy, V. G., Ed., Springer Berlin Heidelberg, 2013, vol. 8025, pp. 108117.
@INCOLLECTION{PWF13,
author = {Puch, Stefan and Wortelen, Bertram and Fr{\"{a}}nzle, Martin and Peikenkamp, Thomas},
editor = {Duffy, Vincent G.},
keywords = {Driver Model, Guided CoSimulation, Hybrid Simulation, Monte Carlo, Risk Analysis},
month = jun, title = {Evaluation of Drivers Interaction with Assistant Systems using Criticality Driven Guided Simulation},
booktitle = {Digital Human Modeling and Applications in Health, Safety, Ergonomics, and Risk Management. Healthcare and Safety of the Environment and Transport},
series = {Lecture Notes in Computer Science},
volume = {8025},
number = {LNCS 80258026},
year = {2013},
pages = {108117},
publisher = {Springer Berlin Heidelberg},
isbn = {9783642391729},
url = {http://dx.doi.org/10.1007/9783642391736_13},
doi = {10.1007/9783642391736_13},
abstract = {Advanced Driver Assistance Systems (ADAS) operate more and more autonomously and take over essential parts of the driving task e.g. keeping safe distance or detecting hazards. Thereby they change the structure of the drivers task and thus induce a change in drivers behavior. Nevertheless it is still the driver who is ultimately responsible for the safe operation of the vehicle. Therefore it is necessary to ensure that the behavioral changes neither reduce the controllability of the vehicle nor the controllability of the hazardous events. We introduce the Threshold Uncertainty Tree Search (TUTS) algorithm as a simulation based approach to explore rare but critical driver behavior in interaction with an assistance system. We present first results obtained with a validated driver model in a simple driving scenario.} } 
[inproceedings] bibtexM. Fakih, K. Grüttner, M. Fränzle, und A. Rettberg, "Exploiting Segregation in BusBased MPSoCs to Improve Scalability of ModelCheckingBased Performance Analysis for SDFAs," in Proc. International Embedded Systems Symposium (IESS), 2013, pp. 205217.
@INPROCEEDINGS{FakihEA:IESS13,
author = {Fakih, Maher and Gr{\"{u}}ttner, Kim and Fr{\"{a}}nzle, Martin and Rettberg, Achim},
title = {Exploiting Segregation in BusBased {MPSoCs} to Improve Scalability of ModelCheckingBased Performance Analysis for {SDFAs}},
booktitle = {International Embedded Systems Symposium (IESS)},
year = {2013},
pages = {205217},
abstract = {The timing predictability of embedded systems with hard realtime requirements is fundamental for guaranteeing their safe usage. With the emergence of multicore platforms this task becomes even more challenging, because of shared processing, communication and memory resources. Modelchecking techniques are capable of verifying the performance properties of applications running on these platforms. Unfortunately, these techniques are not scalable when analyzing systems with large number of tasks and processing units. In this paper, a modelchecking based approach that allows to guarantee timing bounds of multiple Synchronous Data Flow Applications (SDFA) running on shared bus multicore architectures will be extended for a TDMA hypervisor architecture. We will improve the scalability of our modelchecking approach by exploiting the temporal and spatial segregation properties of the TDMA architecture and demonstrate how this method can be applied.} } 
[inproceedings] bibtexM. Fakih, K. Grüttner, M. Fränzle, und A. Rettberg, "Towards Performance Analysis of SDFGs Mapped to SharedBus Architectures Using ModelChecking," in Proc. Proceedings of the Conference on Design, Automation and Test in Europe (DATE) 2013, 3001 Leuven, Belgium, 2013, pp. 11671172.
@INPROCEEDINGS{FakihEA:DATE2013,
author = {Fakih, Maher and Gr{\"{u}}ttner, Kim and Fr{\"{a}}nzle, Martin and Rettberg, Achim},
title = {Towards Performance Analysis of SDFGs Mapped to SharedBus Architectures Using ModelChecking},
booktitle = {Proceedings of the Conference on Design, Automation and Test in Europe (DATE) 2013},
series = {DATE '13},
year = {2013},
pages = {11671172},
publisher = {European Design and Automation Association},
address = {3001 Leuven, Belgium},
abstract = {The timing predictability of embedded systems with hard realtime requirements is fundamental for guaranteeing their safe usage. With the emergence of multicore platforms this task became very challenging. In this paper, a model checking based approach will be described which allows us to guarantee timing bounds of multiple Synchronous Data Flow Graphs (SDFG) running on sharedbus multicore architectures. Our approach utilizes Timed Automata (TA) as a common semantic model to represent software components (SDF actors) and hardware components of the multicore platform. These TA are explored using the UPPAAL modelchecker for providing the timing guarantees. Our approach shows a significant precision improvement compared with the worstcase bounds estimated based on maximal delay for every bus access. Furthermore, scalability is examined to demonstrate analysis feasibility for small parallel systems.} } 
[inproceedings] bibtex  Dokument aufrufenS. Eilers, J. Boger, und M. Fränzle, "A Path Planning Framework for Autonomous Vehicles," in Proc. 9th International Workshop on Robot Motion and Control, 2013, pp. 203208.
@INPROCEEDINGS{Eilers2013_1,
author = {Eilers, S{\"{o}}nke and Boger, J{\"{u}}rgen and Fr{\"{a}}nzle, Martin},
month = jul, title = {A Path Planning Framework for Autonomous Vehicles},
booktitle = {9th International Workshop on Robot Motion and Control},
year = {2013},
pages = {203208},
publisher = {IEEE Explore},
url = {http://dx.doi.org/10.1109/RoMoCo.2013.6614609},
doi = {10.1109/RoMoCo.2013.6614609},
abstract = {In this paper we present a framework for path planning of autonomous vehicles in static environments which allows for rapid prototyping and evaluation. We achieve this by decoupling search based path planning into search on the one hand and expansion strategies on the other hand. Thus we are able to combine arbitrary sampling methods to discretize the search space with arbitrary heuristic search algorithms. Sampling methods and searches can be connected at designtime without the need to recompile the code. Other search algorithms and sampling methods that are programmed against our interfaces can be easily added and combined with existing search algorithms and sampling methods. Furthermore, the framework is capable of creating more complex planners, by adding further sampling/search combinations to planning pipelines. We show the strength of our approach by applying our framework to one particular path planning problem and evaluating three different planning pipelines.},
timestamp={2013.02.07},
} 
[inproceedings] bibtexM. Fränzle und A. Tsourdos, "Preface." , pp. 12.
@INPROCEEDINGS{IntroHAS2011,
author = {Fr{\"{a}}nzle, Martin and Tsourdos, Antonios},
title = {Preface},
pages = {12},
crossref = {HAS2011} } 
[proceedings] bibtexFränzle, Martin and Tsourdos, Antonios, Proceedings of the first workshop on Hybrid Autonomous SystemsElsevier, 2013.
@PROCEEDINGS{HAS2011,
author = {Fr{\"{a}}nzle, Martin and Tsourdos, Antonios},
editor = {Fr{\"{a}}nzle, Martin and Tsourdos, Antonios},
title = {Proceedings of the first workshop on Hybrid Autonomous Systems},
series = {Electronic Notes in Theoretical Computer Science},
volume = {297},
year = {2013},
publisher = {Elsevier} } 
[inproceedings] bibtexM. Kamgarpour, C. Ellen, S. Esmaeil Zadeh Soudjani, S. Gerwinn, J. L. Mathieu, N. Müllner, A. Abate, D. S. Callaway, M. Fränzle, und J. Lygeros, "Modeling Options for Demand Side Participation of Thermostatically Controlled Loads," in Proc. Bulk Power System Dynamics and Control  IX Optimization, Security and Control of the Emerging Power Grid (IREP), 2013 IREP Symposium, 2013, pp. 115.
@INPROCEEDINGS{irep2013,
author = {Kamgarpour, Maryam and Ellen, Christian and Esmaeil Zadeh Soudjani, Sadegh and Gerwinn, Sebastian and Mathieu, Johanna L. and M{\"{u}}llner, Nils and Abate, Alessandro and Callaway, Duncan S. and Fr{\"{a}}nzle, Martin and Lygeros, John},
month = {8},
title = {Modeling Options for Demand Side Participation of Thermostatically Controlled Loads},
booktitle = {Bulk Power System Dynamics and Control  IX Optimization, Security and Control of the Emerging Power Grid (IREP), 2013 IREP Symposium},
year = {2013},
pages = {115},
publisher = {IEEE Xplore},
doi = {10.1109/irep.2013.6629396} } 
[inproceedings] bibtexL. Zou, N. Zhan, S. Wang, M. Fränzle, und S. Qin, "Verifying Simulink Diagrams Via A Hybrid Hoare Logic Prover," in Proc. Proccedings of the 13th International Conference on Embedded Software (EMSOFT), 2013, p. 9:19:10.
@INPROCEEDINGS{Liang:EMSOFT13,
author = {Zou, Liang and Zhan, Naijun and Wang, Shuling and Fr{\"{a}}nzle, Martin and Qin, Shengchao},
editor = {Ernst, Rolf and Sokolsky, Oleg},
title = {Verifying {Simulink} Diagrams Via A Hybrid {Hoare} Logic Prover},
booktitle = {Proccedings of the 13th International Conference on Embedded Software (EMSOFT)},
year = {2013},
pages = {9:19:10},
organization = {ACM},
doi = {10.1109/EMSOFT.2013.6658587},
abstract = {Simulink is an industrial defacto standard for building executable models of embedded systems and their environments, facilitating validation by simulation. Due to the inherent incompleteness of this form of system validation, complementing simulation by formal verification would be desirable. A prerequisite for such an approach is a formal semantics of Simulink's graphical models. In this paper, we show how to encode Simulink diagrams into Hybrid CSP (HCSP), a formal modelling language encoding hybrid system dynamics by means of an extension of CSP. The translation from Simulink to HCSP is fully automatic. We furthermore discuss how to utilize a Hybrid Hoare Logic Prover to verify the translated HCSP models. We demonstrate our approach on a combined scenario originating from the Chinese Highspeed Train Control System at Level 3 (CTCS3).} } 
[inproceedings] bibtexE. Olderog und M. Swaminathan, "Structural Transformations for DataEnriched RealTime Systems," in Proc. integrated Formal Methods (iFM), 2013, pp. 378393.
@INPROCEEDINGS{,
author = {Olderog, ErnstR{\"{u}}diger and Swaminathan, Mani},
keywords = {Communication Closedness, Extended Timed Automata, Flattening, Layered Composition, layred reachability, Noninterference and Precedence, Realtime Mutual Exclusion, Separation},
month = jun, title = {Structural Transformations for DataEnriched RealTime Systems},
booktitle = {integrated Formal Methods (iFM)},
series = {Lecture Notes in Computer Science},
volume = {7940},
year = {2013},
pages = {378393},
publisher = {Springer},
location = {Turku, Finland},
isbn = {9783642386121,97836423861},
doi = {http://dx.doi.org/10.1007/9783642386138_26},
abstract = {We investigate structural transformations for easier verification of realtime systems with shared data variables, modelled as networks of extended timed automata (ETA). Our contributions to this end are: (1) An operator for layered composition of ETA that yields communication closed equivalences under certain independence and / or precedence conditions. (2) Two reachability preserving transformations of separation and flattening for reducing (under certain cycle conditions) the number cycles of the ETA. (3) The interplay of the three structural transformations (separation, flattening, and layering), illustrated on an enhanced version of Fischers realtime mutual exclusion protocol.} }
2012

[article] bibtex  Dokument aufrufenT. Teige und M. Fränzle, "Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems with Applications to Probabilistic State Reachability and Region Stability," Logical Methods in Computer Science, vol. 8, iss. 2, pp. 132, 2012.
@Article{ teigefraenzle:lmcs,
author = {Tino Teige and Martin Fr{\"a}nzle},
title = {Generalized {C}raig Interpolation for Stochastic {B}oolean Satisfiability Problems with Applications to Probabilistic State Reachability and Region Stability},
journal = {Logical Methods in Computer Science},
volume = {8},
number = {2},
year = {2012},
pages = {132},
subproject = {H1/2,H4},
url = {http://www.lmcsonline.org/ojs/viewarticle.php?id=1022\&layout=abstract},
doi = {10.2168/LMCS8(2:16)2012},
abstract = {The stochastic Boolean satisfiability (SSAT) problem has been introduced by Papadimitriou in 1985 when adding a probabilistic model of uncertainty to propositional satisfiability through randomized quantification. SSAT has many applications, among them probabilistic bounded model checking (PBMC) of symbolically represented Markov decision processes. This article identifies a notion of \emph{Craig interpolant} for the SSAT framework and develops an algorithm for computing such interpolants based on a resolution calculus for SSAT. As a potential application area of this novel concept of Craig interpolation, we address the symbolic analysis of probabilistic systems. We first investigate the use of interpolation in probabilistic state reachability analysis, turning the falsification procedure employing PBMC into a verification technique for probabilistic safety properties. We furthermore propose an interpolationbased approach to probabilistic region stability, being able to verify that the probability of stabilizing within some region is sufficiently large.} } 
[inproceedings] bibtex  Dokument aufrufenA. Eggers, N. Ramdani, N. S. Nedialkov, und M. Fränzle, "SetMembership Estimation of Hybrid Systems via SAT Modulo ODE," in Proc. Proceedings of the 16th IFAC Symposium on System Identification, 2012, pp. 440445.
@inproceedings{EggRamNedFra:SYSID:2012,
author = {Andreas Eggers and Nacim Ramdani and Nedialko S. Nedialkov and Martin Fr{\"{a}}nzle},
title = {SetMembership Estimation of Hybrid Systems via {SAT} Modulo {ODE}},
pages = {440445},
booktitle = {Proceedings of the 16th IFAC Symposium on System Identification},
editor = {Michel Kinnaert},
doi = {10.3182/201207113BE2027.00292},
url = {http://dx.doi.org/10.3182/201207113BE2027.00292},
publisher = {The International Federation of Automatic Control (IFAC)},
year = {2012},
abstract = { Set membership estimation (SME) of nonlinear hybrid systems is still a challenging issue. Although SME of nonlinear continuous systems has made significant progress recently, the direct extension of these methods to the hybrid case is not easy. Meanwhile, satisfiability (SAT) checkers for Boolean combinations of arithmetic constraints over real and integervalued variables have made significant progress, as they can effectively deal with algebraic constraints between variables and nonlinear ODEs, what is denoted as SAT Modulo ODE. Finally, the corresponding solvers solve in a natural way the hybrid differential and algebraic constraints satisfaction problems that underlie SME of hybrid systems. This paper presents the application of such a SAT Modulo ODE solver to SME of hybrid dynamical systems.} } 
[inproceedings] bibtexS. Puch, M. Fränzle, J. Osterloh, und C. Läsche, "Rapid VirtualHumanintheLoop Simulation with the High Level Architecture," in Proc. Proceedings of Summer Computer Simulation Conference 2012 (SCSC 2012), Genua, 2012, pp. 4450.
@INPROCEEDINGS{scsc12,
author = {Puch, Stefan and Fr{\"{a}}nzle, Martin and Osterloh, JanPatrick and L{\"{a}}sche, Christoph},
editor = {Bruzzone, A.},
keywords = {Driver Model, Guided Simulation, High Level Architecture (HLA)},
month = {07},
title = {Rapid VirtualHumanintheLoop Simulation with the High Level Architecture},
booktitle = {Proceedings of Summer Computer Simulation Conference 2012 (SCSC 2012)},
volume = {44},
number = {10},
year = {2012},
pages = {4450},
publisher = {Curran Associates, Inc.},
organization = {The Society for Modeling \& Simulation International (SCS)},
address = {Genua},
abstract = {Connecting different simulators, and setting up a distributed simulation is a complex and expensive task. Especially in research projects, where rapid results are desired, this is a task that is often too time consuming. Therefore the use of standards and existing frameworks can be helpful. The IEEE 1516 High Level Architecture (HLA) is a wellestablished concept for distributed simulation, whereas HLA is not well suited for rapid prototyping. In this paper, we describe how we use HLA in a virtualhumanintheloop simulation, as well as the framework we developed in order to allow to rapidly connect new simulators. Finally, we present an evaluation of our framework, which shows that an open source RTI in our context of research may compete well with a commercial RTI implementation.} } 
[inproceedings] bibtexC. Ellen, S. Gerwinn, und M. Fränzle, "Confidence Bounds for Statistical Model Checking of Probabilistic Hybrid Systems," in Proc. Proceedings of the 10th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), 2012, pp. 123138.
@INPROCEEDINGS{Ellen2012,
author = {Ellen, Christian and Gerwinn, Sebastian and Fr{\"a}nzle, Martin},
title = {Confidence Bounds for Statistical Model Checking of Probabilistic Hybrid Systems},
booktitle = {Proceedings of the 10th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS)},
year = {2012},
editor = {Jurdzi{\'n}ski, Marcin and Nickovic, Dejan},
volume = {7595},
series = {LNCS},
pages = {123138},
publisher = {Springer},
owner = {cellen},
timestamp = {2012.07.20} } 
[inproceedings] bibtexS. Eilers, S. Gerwinn, M. Fränzle, C. Kuka, S. Schweiger, und T. Toben, "An Autonomous Vehicle Design for Safe Operation in Heterogeneous Environments," in Proc. Proceedings of The CONCUR '12 Workshop on Trustworthy CyberPhysical Systems, 2012, pp. 3137.
@INPROCEEDINGS{Eilers2012,
author = {Eilers, S{\"o}nke and Gerwinn, Sebastian and Fr{\"a}nzle, Martin and Kuka, Christian and Schweiger, S{\"o}ren and Toben, Tobe},
Title = {An Autonomous Vehicle Design for Safe Operation in Heterogeneous Environments},
Year = {2012},
Pages = {31  37},
Month = {08},
Editor = {Fitzgerald, John and Mak, Terrence and Romanovsky, Alexander and Yakovlev, Alex},
Series = {Technical Report Series},
Booktitle = {Proceedings of The CONCUR '12 Workshop on Trustworthy CyberPhysical Systems},
Institution = {Newcastle University, UK} } 
[article] bibtexM. Swaminathan, J. Katoen, und E. Olderog, "Layered Reasoning for Randomized Distributed Algorithms," Formal Aspects of Computing, vol. 24, iss. 46, pp. 477496, 2012.
@ARTICLE{swakatold:2012,
author = {Swaminathan, Mani and Katoen, JoostPieter and Olderog, ErnstR{\"{u}}diger},
keywords = {Probabilistic automata – Layered composition and separation – Communication closedness – Partial order equivalence – Randomizedmutual exclusion},
month = jul, title = {Layered Reasoning for Randomized Distributed Algorithms},
journal = {Formal Aspects of Computing},
volume = {24},
number = {46},
year = {2012},
pages = {477496},
doi = {http://dx.doi.org/10.1007/s001650120231x},
abstract = {This paper adopts the communication closed layer (CCL) concept of Elrad and Francez to the formal reasoning of randomized distributed algorithms. We do so by enriching probabilistic automata (PA) with a layered composition operator, an intermediate between parallel and sequential composition. Layered composition is used to establish probabilistic counterparts of the CCL laws that exploit independence and/or precedence conditions between the constituent PA. The probabilistic CCL laws enable partial order (po) equivalence when layered composition is replaced by sequential composition. Such poequivalence induces a purely syntactic partialorder state space reduction via layered separation in compositions of PA while preserving probabilistic nextfree lineartime properties. The feasibility of such layered separation is demonstrated on a randomized mutual exclusion algorithm by Kushilevitz and Rabin, complementing an algebraic approach (for analyzing this algorithm) by McIver, Gonzalia, Cohen, and Morgan.} } 
[inproceedings] bibtexS. Puch, B. Wortelen, M. Fränzle, und T. Peikenkamp, "Using Guided Simulation to Improve a ModelBased Design Process of Complex Human Machine Systems," in Proc. ESM'2012  The 2012 European Simulation And Modelling Conference, Essen, 2012, pp. 159164.
@INPROCEEDINGS{esm2012,
author = {Stefan Puch and Bertram Wortelen and Martin Fr{\"{a}}nzle and Thomas Peikenkamp},
title = {Using Guided Simulation to Improve a ModelBased Design Process of Complex Human Machine Systems},
booktitle = {ESM'2012  The 2012 European Simulation And Modelling Conference},
year = {2012},
editor = {M. Klumpp},
pages = {159164},
address = {Essen},
month = {10},
isbn = {9789077381711},
publisher = {EUROSISETI},
abstract = {Modelbased risk assessment of human machine systems in safety critical environments is a difficult task. The complexity of the system and the inherent probabilistic nature of the human operators make an exhaustive formal analysis infeasible. In this paper a concept for an efficient exploration of critical situations is presented. Two algorithms for identification of critical situations and estimation of their probabilities are introduced. Complexity is handled by an intelligent guidance strategy and an adjustable concept of abstraction. We discuss advantages and shortcomings of our approach on a theoretical level. Finally, an evaluation plan of the presented concept is outlined. It will investigate the effects of a driver assistance system in a system incorporating a driver, a car and its environment. This study utilizes a detailed cognitive driver model for the driver component of the system.} } 
[article] bibtex  Dokument aufrufenA. Eggers, N. Ramdani, N. S. Nedialkov, und M. Fränzle, "Improving the SAT Modulo ODE Approach to Hybrid Systems Analysis by Combining Different Enclosure Methods," Software and Systems Modeling, 2012 to appear. Copyright: SpringerVerlag Berlin Heidelberg, 2012. The final publication is available at www.springerlink.com..
@article{eggramnedfra:sosym:2012,
author = {Andreas Eggers and Nacim Ramdani and Nedialko S. Nedialkov and Martin Fr{\"{a}}nzle},
title = {Improving the {SAT} Modulo {ODE} Approach to Hybrid Systems Analysis by Combining Different Enclosure Methods},
journal = {Software and Systems Modeling},
doi = {10.1007/s1027001202953},
publisher = {Springer},
year = {2012 to appear. Copyright: SpringerVerlag Berlin Heidelberg, 2012. The final publication is available at www.springerlink.com.},
note = {accepted for publication, to appear. Copyright: SpringerVerlag Berlin Heidelberg, 2012. The final publication is available at www.springerlink.com.},
abstract = {Aiming at automatic verification and analysis techniques for hybrid discretecontinuous systems, we present a novel combination of enclosure methods for ordinary differential equations (ODEs) with the iSAT solver for large Boolean combinations of arithmetic constraints. Improving on our previous work, the contribution of this paper lies in combining iSAT with VNODELP, as a stateoftheart interval solver for ODEs, and with bracketing systems, which exploit monotonicity properties allowing to find enclosures for problems that VNODELP alone cannot enclose tightly. We apply the combined iSATODE solver to the analysis of a variety of nonlinear hybrid systems by solving predicative encodings of reachability properties and of an inductive stability argument, and evaluate the impact of the different enclosure methods, decision heuristics, and their combination. Our experiments include classic benchmarks from the literature, as well as a newlydesigned conveyor belt system that combines hybrid behavior of parallel components, a slipstick friction model with nonlinear dynamics and flow invariants, and several dimensions of parameterization. In the paper, we also present and evaluate an extension of VNODELP tailored to its use as a deduction mechanism within iSATODE, to allow fast reevaluations of enclosures over arbitrary subranges of the analyzed time span.},
url = {http://hs.informatik.unioldenburg.de/download/eggramnedfra_sosys_2012_authors_copy.pdf} } 
[phdthesis] bibtex  Dokument aufrufenT. Teige, "Stochastic Satisfiability Modulo Theories: A Symbolic Technique for the Analysis of Probabilistic Hybrid Systems," PhD Thesis , Germany, 2012.
@PhdThesis{Teige12:PhDThesis,
author = {Tino Teige},
title = {Stochastic Satisfiability Modulo Theories: A Symbolic Technique for the Analysis of Probabilistic Hybrid Systems},
school = {Carl von Ossietz\ky Universit{\"a}t Oldenburg, Department of Computing Science},
year = {2012},
type = {Doctoral Dissertation},
address = {Germany},
note = {Supervisors: Prof.~Dr.~Martin Fr{\"a}nzle and Prof.~Dr.Ing.~Holger Hermanns},
url = {http://oops.unioldenburg.de/1389/} } 
[inproceedings] bibtexN. Müllner, O. Theel, und M. Fränzle, "Combining Decomposition and Reduction for State Space Analysis of a SelfStabilizing System," in Proc. Proceedings of the 2012 IEEE 26th International Conference on Advanced Information Networking and Applications, 2012, pp. 936943.
@INPROCEEDINGS{Muellner2012,
author = {M{\"{u}}llner, Nils and Theel, Oliver and Fr{\"{a}}nzle, Martin},
keywords = {chain state space, Detectors, distributed processing , distributed system, exponential growth, fault tolerance, fault tolerance property verification, fault tolerant computing, Fault tolerant systems, formal verification, lumped Markov chain, lumping, lumping piecewise, Markov chains, Markov processes, probabilistic logic, reduction technique, redundant information, Registers, selfstabilization, selfstabilizing system, state space analysis, state space reduction, statespace methods, system decomposition, Transient analysis},
month = mar, title = {Combining Decomposition and Reduction for State Space Analysis of a SelfStabilizing System},
booktitle = {Proceedings of the 2012 IEEE 26th International Conference on Advanced Information Networking and Applications},
year = {2012},
pages = {936  943},
publisher = {IEEE Computer Society},
location = {Fukuokashi, Fukuoka, Japan},
organization = {IEEE},
note = {Best Paper Award},
issn = {1550445X},
doi = {10.1109/AINA.2012.127},
abstract = {Verifying fault tolerance properties of a distributed system can be achieved by state space analysis via Markov chains. Yet, the power of such exact analytic methods is very limited as the state space is exponentially proportional to the system size. We propose a method that alleviates this limit. Lumping is a well known reduction technique that can be applied to a Markov chain to prune redundant information. We propose a system decomposition to employ lumping piecewise on the considerably smaller Markov chains of the subsystems which are much more likely to be tractable. Recomposing the lumped Markov chains of the subsystems results in a configuration space that is likely to be considerably smaller. An example demonstrates how the limiting window availability (i.e. a fault tolerance property) can be computed for a system while exploiting the combination of lumping and decomposition.} } 
[incollection] bibtexM. Fränzle, "An Introduction to Interval Methods," in Modern Computational Science, Leidl, R. und Hartmann, A., Eds., Oldenburger Universitätsverlag, 2012, pp. 207222.
@INCOLLECTION{MCS12:IntervalMethods,
author = {Fr{\"{a}}nzle, Martin},
editor = {Leidl, Reinhard and Hartmann, Alexander},
title = {An Introduction to Interval Methods},
booktitle = {Modern Computational Science},
year = {2012},
pages = {207222},
publisher = {Oldenburger Universit{\"{a}}tsverlag} } 
[inproceedings] bibtexC. Ellen, E. Christoph, und M. Oertel, "Automatic Transition Between Structural System Views in a Safety Relevant Embedded Systems Development Process," in Proc. Proceedings of the Conference on Design, Automation and Test in Europe, 3001 Leuven, Belgium, 2012, pp. 820824.
@INPROCEEDINGS{Ellen2012b,
author = {Ellen, Christian and Christoph, Etzien and Oertel, Markus},
month = {03},
title = {Automatic Transition Between Structural System Views in a Safety Relevant Embedded Systems Development Process},
booktitle = {Proceedings of the Conference on Design, Automation and Test in Europe},
series = {DATE '12},
year = {2012},
pages = {820824},
publisher = {European Design and Automation Association},
address = {3001 Leuven, Belgium},
isbn = {9783981080186},
abstract = {It is mandatory to design safety relevant embedded systems in multiple structural system views. A typical example is the usage of a functional and technical system representation. A transition between these system views not only comprises the allocation of components but also copes with multiple design aspects and constraints that need to be transferred to the target perspective. Optimization goals regarding arbitrary design artifacts complicate this problem. In this paper we present a novel comprehensive approach integrating common allocation techniques together with a partial design generation in a system wide process to optimize complex system view transitions. We demonstrate our approach using the CESAR design methodology. The original system models and requirements are used as input for our procedure and the results are directly applied to the same models.} }
2011

[techreport] bibtexT. Teige und M. Fränzle, "Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems," SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 67, 2011.
@techreport{TeigeFraenzle:ATR67,
author = {Tino Teige and Martin Fr{\"a}nzle},
title = {Generalized {C}raig Interpolation for Stochastic {B}oolean Satisfiability Problems},
editor = {Bernd Becker and Werner Damm and Bernd Finkbeiner and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski},
institution = {SFB/TR 14 AVACS},
month = {March},
year = {2011},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
number = {67},
note = {ISSN: 18609821, http://www.avacs.org.},
} 
[inproceedings] bibtexT. Teige, "Stochastic Satisfiability Modulo Theories: A Technique for the Analysis of Probabilistic Hybrid Systems," in Proc. Joint Workshop of the German Research Training Groups in Computer Science, 2011, p. 47.
@InProceedings{TeigeDagstuhl11:SSMT,
author = {Tino Teige},
title = {Stochastic Satisfiability Modulo Theories: A Technique for the Analysis of Probabilistic Hybrid Systems},
booktitle = {Joint Workshop of the German Research Training Groups in Computer Science},
editor = {Johannes H\"olzl and Liz RibeBaumann and Markus Br\"uckner},
year = {2011},
pages = {47},
publisher = {Gito Verlag},
note = {ISBN: 9783942183369} } 
[inproceedings] bibtexS. Kupferschmid, B. Becker, T. Teige, und M. Fränzle, "Proof Certificates and Nonlinear Arithmetic Constraints," in Proc. Proceedings of the 14th IEEE Symposium on Design and Diagnostics of Electronic Circuits and Systems (DDECS 2011), 2011.
@InProceedings{KupferschmidEtAl:DDECS11,
author = {Stefan Kupferschmid and Bernd Becker and Tino Teige and Martin Fr{\"a}nzle},
title = {Proof Certificates and Nonlinear Arithmetic Constraints},
booktitle = {Proceedings of the 14th IEEE Symposium on Design and Diagnostics of Electronic Circuits and Systems (DDECS 2011)},
year = {2011},
publisher = {IEEE},
} 
[inproceedings] bibtexT. Teige und M. Fränzle, "Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems," in Proc. Proceedings of the Seventeenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2011, pp. 158172.
@InProceedings{TeigeFraenzle:TACAS11,
author = {Tino Teige and Martin Fr{\"a}nzle},
title = {Generalized {C}raig Interpolation for Stochastic {B}oolean Satisfiability Problems},
editor = {Parosh Aziz Abdulla and K. Rustan M. Leino},
booktitle = {Proceedings of the Seventeenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
year = {2011},
pages = {158172},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6605},
} 
[article] bibtexT. Teige, A. Eggers, und M. Fränzle, "ConstraintBased Analysis of Concurrent Probabilistic Hybrid Systems: An Application to Networked Automation Systems," Nonlinear Analysis: Hybrid Systems, vol. 5, iss. 2, pp. 343366, 2011.
@ARTICLE{TeiEggFra:NAHS,
author = {Teige, Tino and Eggers, Andreas and Fr{\"{a}}nzle, Martin},
editor = {Giu, Allessandro and Silva, Manuel and Zaytoon, Janan},
keywords = {automatic verification, concurrent probabilistic hybrid systems, constraint satisfaction problems, probabilistic logic, problem solvers},
month = may, title = {ConstraintBased Analysis of Concurrent Probabilistic Hybrid Systems: An Application to Networked Automation Systems},
journal = {Nonlinear Analysis: Hybrid Systems},
volume = {5},
number = {2},
year = {2011},
pages = {343366},
publisher = {Elsevier},
issn = {1751570x},
doi = {10.1016/j.nahs.2010.04.009},
abstract = {In previous publications, the authors have introduced the notion of stochastic satisfiability modulo theories (SSMT) and the corresponding SiSAT solving algorithm, which provide a symbolic method for the reachability analysis of probabilistic hybrid systems. SSMT extends satisfiability modulo theories (SMT) with randomized (or stochastic), existential, and universal quantification, as known from stochastic propositional satisfiability. In this paper, we extend the SSMTbased procedures to the symbolic analysis of concurrent probabilistic hybrid systems. After formally introducing the computational model, we provide a mechanized translation scheme to encode probabilistic bounded reachability problems of concurrent probabilistic hybrid automata as linearly sized SSMT formulae, which in turn can be solved by the SiSAT tool. We furthermore propose an algorithmic enhancement which tailors SiSAT to probabilistic bounded reachability problems by caching and reusing solutions obtained on bounded reachability problems of smaller depth. An essential part of this article is devoted to a case study from the networked automation systems domain. We explain in detail the formal model in terms of concurrent probabilistic automata, its encoding into the SiSAT modeling language, and finally the automated quantitative analysis.},
access={restricted},
subproject={H1/2,H4} } 
[inproceedings] bibtexM. Fränzle, T. Gezgin, H. Hungar, S. Puch, und G. Sauter, "Predicting the Effect of Driver Assistance via Simulation," in Proc. Human Modelling in Assisted Transportation, 2011, pp. 299306.
@INPROCEEDINGS{FGH10,
author = {Martin Fr{\"a}nzle and Tayfun Gezgin and Hardi Hungar and Stefan Puch and Gerald Sauter},
title = {Predicting the Effect of Driver Assistance via Simulation},
booktitle = {Human Modelling in Assisted Transportation},
year = {2011},
pages = {299306},
editor = {P.C. Cacciabue and M. Hj{\"a}lmdahl and A. L{\"u}dtke and C. Riccioli},
publisher = {Springer},
abstract = {Developing assistance systems in the automotive domain involves several exploration and evaluation activities with potential users of the system. To replace the amount of human test subject involvement, executable models reproducing human behaviour are introduced. Together with models of the car, road, surrounding traffic and of course the assistance system, a complete representation of the assistance system in its application environment can then be constructed which may be used to predict effects of introducing the assistance without having to resort to experiments with humans. In this paper we present techniques concerned with the exploration of the behaviour spectrum of the combined models. We show how functionality and safety aspects of assisted driving can be evaluated in computer simulations already during early phases of the development process.} } 
[techreport] bibtexN. T. Dinh, M. Fränzle, und A. Eggers, "AVACS H1/2 8year Benchmark: Analyzing Traffic Models With iSAT," SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 81, 2011.
@TECHREPORT{atr081,
author = {Dinh, Nam Thang and Fr{\"{a}}nzle, Martin and Eggers, Andreas},
editor = {Becker, Bernd and Damm, Werner and Finkbeiner, Bernd and Fr{\"{a}}nzle, Martin and Olderog, ErnstR{\"{u}}diger and Podelski, Andreas},
keywords = {benchmark, HySAT, iSAT, traffic modelling},
month = {July},
title = {{AVACS H1/2} 8year Benchmark: Analyzing Traffic Models With {iSAT}},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
number = {81},
year = {2011},
institution = {SFB/TR 14 AVACS},
note = {ISSN: 18609821, http://www.avacs.org},
abstract = {In this technical report, we present an application of the iSAT constraint solver to instances of traffic flow networks.We give an account of the underlying model and provide details of different instances of the model and a variety of verification and falsification tasks handled by our solver.} } 
[inproceedings] bibtexA. Eggers, E. Kruglov, S. Kupferschmid, K. Scheibler, T. Teige, und C. Weidenbach, "Superposition Modulo NonLinear Arithmetic," in Proc. 8th international Symposium on Frontiers of Combining Systems (FroCos 2011), 2011, pp. 119134.
@INPROCEEDINGS{eggersetalfrocos2011,
author = {Eggers, Andreas and Kruglov, Evgeny and Kupferschmid, Stefan and Scheibler, Karsten and Teige, Tino and Weidenbach, Christoph},
keywords = {iSAT, SPASS, SPASS(iSAT), SUP(T)},
title = {Superposition Modulo NonLinear Arithmetic},
booktitle = {8th international Symposium on Frontiers of Combining Systems (FroCos 2011)},
series = {Lecture Notes in Computer Science},
year = {2011},
publisher = {Springer},
pages = {119134},
doi = {10.1007/9783642243646_9},
volume = {6989},
abstract = {The firstorder theory over nonlinear arithmetic including transcendental functions (NLA) is undecidable. Nevertheless, in this paper we show that a particular combination with superposition leads to a sound and complete calculus that is useful in practice. We follow basically the ideas of the SUP(LA) combination, but have to take care of undecidability, i.e., ``unknown'' answers by the NLA reasoning procedure. A pipeline of NLA constraint simplification techniques related to the SUP(NLA) framework significantly decreases the number of ``unknown'' answers. The resulting approach is implemented as SUP(NLA) by a system combination of Spass and iSAT. Applied to various scenarios of traffic collision avoidance protocols, we show by experiments that Spass(iSAT) can fully automatically proof and disproof safety properties of such protocols using the very same formalization.} } 
[inproceedings] bibtexA. Eggers, N. Ramdani, N. S. Nedialkov, und M. Fränzle, "Improving SAT Modulo ODE for Hybrid Systems Analysis by Combining Different Enclosure Methods," in Proc. Proceedings of the Ninth International Conference on Software Engineering and Formal Methods (SEFM), 2011, pp. 172187.
@INPROCEEDINGS{eggramnedfra:sefm:2011,
author = {Eggers, Andreas and Ramdani, Nacim and Nedialkov, Nedialko S. and Fr{\"{a}}nzle, Martin},
keywords = {bounded model checking, bracketing systems, direction deduction, hybrid systems, integration of ordinary differential equations, iSAT(ODE), Sat Modulo Theories, twotank system, VNODELP. iSAT},
title = {Improving {SAT} Modulo {ODE} for Hybrid Systems Analysis by Combining Different Enclosure Methods},
booktitle = {Proceedings of the Ninth International Conference on Software Engineering and Formal Methods (SEFM)},
series = {Lecture Notes in Computer Science},
year = {2011},
pages = {172187},
doi = {10.1007/9783642246906_13},
volume = {7041},
publisher = {Springer},
abstract = {Aiming at automatic verification and analysis techniques for hybrid systems, we present a novel combination of enclosure methods for ordinary differential equations (ODEs) with the iSAT solver for Boolean combinations of arithmetic constraints. Improving on our previous work, the contribution of this paper lies in combining iSAT with VNODELP, as a stateoftheart enclosure method for ODEs, and with bracketing systems whichby exploiting monotonicity properties of the systemallow finding enclosures for problems that VNODELP alone cannot enclose tightly. We apply our method to the analysis of a nonlinear hybrid system by solving predicative encodings of an inductive stability argument and evaluate the impact of different methods and their interplay in combination.} } 
[inproceedings] bibtexW. Damm, M. Fränzle, und J. Quesel, "Crossing the Bridge between Similar Games," in Proc. Formal Modeling and Analysis of Timed Systems  9th International Conference (FORMATS), Aalborg, Denmark, 2123 September, 2011. Proceedings, 2011, pp. 160176.
@INPROCEEDINGS{avacsh3brg11,
author = {Damm, W. and Fr{\"{a}}nzle, Martin and Quesel, JanDavid},
editor = {Tripakis, Stavros and Fahrenberg, Uli},
keywords = {formal verification of hybrid systems, hybrid games, logics for hybrid systems, robust simulation},
month = sep, title = {Crossing the Bridge between Similar Games},
booktitle = {Formal Modeling and Analysis of Timed Systems  9th International Conference (FORMATS), Aalborg, Denmark, 2123 September, 2011. Proceedings},
series = {Lecture Notes in Computer Science (LNCS)},
volume = {6919},
year = {2011},
pages = {160176},
publisher = {SpringerVerlag},
issn = {9783642243097},
doi = {10.1007/9783642243103_12},
abstract = {Specifications and implementations of complex physical systems tend to differ as low level effects such as sampling are often ignored when high level models are created. Thus, the low level models are often not exact refinements of the high level specification. However, they are similar to those. To bridge the gap between those models, we study robust simulation relations for hybrid systems. In this paper, we identify a family of robust simulation relations that allow for certain bounded deviations in the behavior of a system specification and its implementation in both values of the system variables and timings. We show that for this relaxed version of simulation a broad class of logical properties is preserved. The question whether two systems are in simulation relation can be reduced to a reach avoid problem for hybrid games. We provide a sufficient condition under which a winning strategy for these games exists.} } 
[incollection] bibtexM. Fränzle und C. Lengauer, "Semantic Independence," in Encyclopedia of Parallel Computing, Padua, D. und others, Eds., SpringerVerlag, 2011, pp. 18031810.
@incollection{FraLen11svSemInd,
author = {Martin Fr{\"a}nzle and Christian Lengauer},
title = {Semantic Independence},
booktitle = {Encyclopedia of Parallel Computing},
publisher = {SpringerVerlag},
year = {2011},
editor = {David Padua and others},
month = {sep},
pages = {18031810} } 
[book] bibtexC. Herde, Efficient Solving of Large Arithmetic Constraint Systems with Complex Boolean Structure  Proof Engines for the Analysis of Hybrid DiscreteContinuous Systems, 1st ed., Vieweg+Teubner Research, 2011.
@BOOK{herde:2011:phd,
author = {Herde, Christian},
title = {Efficient Solving of Large Arithmetic Constraint Systems with Complex Boolean Structure  Proof Engines for the Analysis of Hybrid DiscreteContinuous Systems},
edition = {1st},
year = {2011},
publisher = {Vieweg+Teubner Research},
school = {Carl von Ossietzky Universit{\"{a}}t Oldenburg},
isbn = {9783834814944} } 
[inproceedings] bibtex  Dokument aufrufenM. Fränzle, E. M. Hahn, H. Hermanns, N. Wolovick, und L. Zhang, "Measurability and safety verification for stochastic hybrid systems," in Proc. Proceedings of the 14th international conference on Hybrid systems: computation and control, New York, NY, USA, 2011, pp. 4352.
@inproceedings{Franzle:2011:MSV:1967701.1967710,
author = {Fr\"{a}nzle, Martin and Hahn, Ernst Moritz and Hermanns, Holger and Wolovick, Nicol\'{a}s and Zhang, Lijun},
title = {Measurability and safety verification for stochastic hybrid systems},
booktitle = {Proceedings of the 14th international conference on Hybrid systems: computation and control},
series = {HSCC '11},
year = {2011},
isbn = {9781450306294},
location = {Chicago, IL, USA},
pages = {4352},
numpages = {10},
url = {http://doi.acm.org/10.1145/1967701.1967710},
doi = {http://doi.acm.org/10.1145/1967701.1967710},
acmid = {1967710},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {measurability, nondeterministic markov process, probabilistic hybrid automaton, reachability, stochastic hybrid automaton},
} 
[article] bibtexE. Ábrahám, T. Schubert, B. Becker, M. Fränzle, und C. Herde, "Parallel SAT Solving in Bounded Model Checking," Journal of Logic and Computation, vol. 21, iss. 1, pp. 521, 2011.
@ARTICLE{AbrahamEA11,
author = {{\'{A}}brah{\'{a}}m, Erika and Schubert, Tobias and Becker, Bernd and Fr{\"{a}}nzle, Martin and Herde, Christian},
keywords = {bounded model checking, hybrid systems, linear programming, parallel programs, SAT solving},
title = {Parallel {SAT} Solving in Bounded Model Checking},
journal = {Journal of Logic and Computation},
volume = {21},
number = {1},
year = {2011},
pages = {521},
publisher = {Oxford University Press},
doi = {10.1093/logcom/exp002},
abstract = {Bounded model checking (BMC) is an incremental refutation technique to search for counterexamples of increasing length. The existence of a counterexample of a fixed length is expressed by a firstorder logic formula that is checked for satisfiability using a suitable solver. We apply communicating parallel solvers to check satisfiability of the BMC formulae. In contrast to other parallel solving techniques, our method does not parallelize the satisfiability check of a single formula, but the parallel solvers work on formulae for different counterexample lengths. We adapt the method of constraint sharing and replication of Shtrichman, originally developed for sequential BMC, to the parallel setting. Since the learning mechanism is now parallelized, it is not obvious whether there is a benefit from the concepts of Shtrichman in the parallel setting. We demonstrate on a number of benchmarks that adequate communication between the parallel solvers yields the desired results.},
subproject={H1/2},
access={restricted},
}
2010

[inproceedings] bibtex  Dokument aufrufenT. Teige und M. Fränzle, "Resolution for Stochastic Boolean Satisfiability," in Proc. Logic for Programming, Artificial Intelligence, and Reasoning, 17th International Conference (LPAR17), 2010, pp. 625639.
@InProceedings{TeiFrae:LPAR17,
author = {Tino Teige and Martin Fr{\"a}nzle},
title = {Resolution for Stochastic {B}oolean Satisfiability},
booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 17th International Conference (LPAR17)},
editor = {Christian Ferm{\"u}ller and Andrei Voronkov},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6397},
pages = {625639},
year = {2010},
doi = {10.1007/9783642162428_44},
url = {http://dx.doi.org/10.1007/9783642162428_44} } 
[inproceedings] bibtex  Dokument aufrufenM. Fränzle, T. Teige, und A. Eggers, "Satisfaction Meets Expectations: Computing Expected Values of Probabilistic Hybrid Systems with SMT," in Proc. Integrated Formal Methods 2010, 2010, pp. 168182.
@InProceedings{FraTeiEgg:iFM10,
author = {Martin Fr{\"a}nzle and Tino Teige and Andreas Eggers},
title = {Satisfaction Meets Expectations: Computing Expected Values of Probabilistic Hybrid Systems with SMT},
booktitle = {Integrated Formal Methods 2010},
editor = {Dominique M{\'e}ry and Stephan Merz},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6396},
pages = {168182},
year = {2010},
subproject = {H1/2,H4},
doi = {10.1007/9783642162657},
url = {http://dx.doi.org/10.1007/9783642162657},
abstract = {Stochastic satisfiability modulo theories (SSMT), which is an extension of satisfiability modulo theories with randomized quantification, has successfully been used as a symbolic technique for computing reachability probabilities in probabilistic hybrid systems. Motivated by the fact that several industrial applications call for quantitative measures that go beyond mere reachability probabilities, this paper extends SSMT to compute expected values of probabilistic hybrid systems like, e.g., meantimes to failure. Practical applicability of the proposed approach is demonstrated by a case study from networked automation systems.},
} 
[article] bibtex  Dokument aufrufenM. Fränzle, T. Teige, und A. Eggers, "Engineering Constraint Solvers for Automatic Analysis of Probabilistic Hybrid Automata," Journal of Logic and Algebraic Programming, vol. 79, pp. 436466, 2010.
@Article{FraTeiEgg:JLAP,
author = {Martin Fr{\"a}nzle and Tino Teige and Andreas Eggers},
title = {Engineering Constraint Solvers for Automatic Analysis of Probabilistic Hybrid Automata},
journal = {Journal of Logic and Algebraic Programming},
editor = {Tarmo Uustalu and J{\"u}ri Vain},
volume = {79},
pages = {436466},
publisher = {Elsevier},
year = {2010},
keywords = {Probabilistic hybrid automata, bounded model checking, arithmetic constraint solving, stochastic satisfiability},
subproject = {H1/2,H4},
doi = {10.1016/j.jlap.2010.07.003},
url = {http://dx.doi.org/10.1016/j.jlap.2010.07.003},
abstract = {In this article, we recall different approaches to the constraintbased, symbolic analysis of hybrid discretecontinuous systems and combine them to a technology able to address hybrid systems exhibiting both nondeterministic and probabilistic behavior akin to infinitestate Markov decision processes. To enable mechanized analysis of such systems, we extend the reasoning power of arithmetic satisfiabilitymodulotheories (SMT) solving by, first, reasoning over ordinary differential equations (ODEs) and, second, a comprehensive treatment of randomized (also known as stochastic) quantification over discrete variables as well as existential quantification over both discrete and continuous variables within the mixed Booleanarithmetic constraint system. This provides the technological basis for a constraintbased analysis of densetime probabilistic hybrid automata, extending previous results addressing discretetime automata (1). Generalizing SMTbased bounded modelchecking of hybrid automata (2; 3), stochastic SMT including ODEs permits the direct analysis of probabilistic bounded reachability problems of densetime probabilistic hybrid automata without resorting to approximation by intermediate finitestate abstractions.} } 
[techreport] bibtex  Dokument aufrufenS. Puch, G. Sauter, und M. Fränzle, "HLAbasierte Kosimulation domänentypischer Simulatoren," Carl von Ossietzky Universität Oldenburg2010.
@TECHREPORT{PuchEA:TechReport,
author = {Stefan Puch and Gerald Sauter and Martin Fr{\"a}nzle},
title = {{HLAbasierte Kosimulation dom{\"a}nentypischer Simulatoren}},
institution = {Carl von Ossietzky Universit{\"a}t Oldenburg},
url = {http://imost.informatik.unioldenburg.de/download/TecReport_IMoST_002.pdf},
year = {2010},
} 
[inproceedings] bibtexJ. Gacnik, H. Jost, F. Köster, und M. Fränzle, "The DeSCAS Methodology and Lessons Learned on Applying Formal Reasoning to Safety Domain Knowledge," in Proc. Proceedings of the 8th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT 2010), 2010.
@INPROCEEDINGS{GaJoKoFr:FORMS10,
author = {Jan Gacnik and Henning Jost and Frank K{\"o}ster and Martin Fr{\"a}nzle},
title = {{The DeSCAS Methodology and Lessons Learned on Applying Formal Reasoning to Safety Domain Knowledge}},
booktitle = {{Proceedings of the 8th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT 2010)}},
year = {2010},
editor = {Eckehard Schnieder and G\'{e}za Tarnai},
abstract = {Functional safety has become an important aspect for engineering activities in the automotive domain due to the upcoming introduction of the safety standard ISO 26262. This paper proposes a methodology to guide the safety related requirements engineering process by means of OWL (Web Ontology Language) ontologies. These ontologies formalize necessary domain knowledge and serve as reference models to support semiautomated requirements discovery and to ease the certification process. Using OWL's logical base, knowledge inference is applied to reason about safety measures for ensuring compliance with the reference process (guidance). The proposed methodology has been implemented in a prototype toolchain and applied to a simple lane departure warning system as an example assistance and automation system. Lessons learned refer to conceptual (expressiveness) and technical (tooling efficiency) issues.} } 
[inproceedings] bibtex  Dokument aufrufenM. Fränzle, T. Gezgin, H. Hungar, S. Puch, und G. Sauter, "Using Guided Simulation to Assess Driver Assistance Systems," in Proc. Proc. FORMS/FORMAT 2010, 2010.
@INPROCEEDINGS{FGH10b,
author = {Martin Fr{\"a}nzle and Tayfun Gezgin and Hardi Hungar and Stefan Puch and Gerald Sauter},
title = {Using Guided Simulation to Assess Driver Assistance Systems},
booktitle = {Proc. FORMS/FORMAT 2010},
year = {2010},
editor = {E. Schnieder and G. Tarnai},
abstract = {The goal of our approach is the modelbased prediction of the effects of driver assistance systems. Starting with the integration of a computer model of the driver of a car into a simulation environment, we face the problem of analysing the emergent effects of a complex system with discrete, numeric and probabilistic components. In particular, it is difficult to assess the probability of rare events, though we are specifically interested in critical situations which will be infrequent for any reasonable system. For that purpose, we use a quantitative logic which enables us to specify criticality and other properties of simulation runs. An online evaluation of the logic permits us to define a procedure which guides the simulation towards critical situations and allows to estimate the risk of connected with the introduction of the assistance system.},
url = {http://hs.informatik.unioldenburg.de/download/HungarEtAlFORMS2010pub.pdf} } 
[inproceedings] bibtex  Dokument aufrufenA. Eggers, "SAT Modulo ODE: A Direct SAT approach to Hybrid Systems," in Proc. 10271 Abstracts Collection  Verification over discretecontinuous boundaries, Dagstuhl, Germany, 2010, pp. 78.
@inproceedings{eggers:satmoduloode:dagstuhl:10271:2010,
author = {Andreas Eggers},
title = {{SAT} Modulo {ODE}: A Direct {SAT} approach to Hybrid Systems},
booktitle = {10271 Abstracts Collection  Verification over discretecontinuous boundaries},
editor = {Bernd Becker and Luca Cardelli and Holger Hermanns and Sofiene Tahar},
series = {Dagstuhl Seminar Proceeding},
number = {10271},
year = {2010},
publisher = {Schloss Dagstuhl  LeibnizZentrum fuer Informatik, Germany},
address = {Dagstuhl, Germany},
pages = {78},
ISSN = {18624405},
subproject= {H1/2},
bibtex = {eggers.dagstuhl10.bib},
url = {http://drops.dagstuhl.de/opus/volltexte/2010/2792},
abstract = {In this talk, we present our approach to perform bounded model checking (BMC) of hybrid discrete continuous systems using constraint solving techniques. The BMC problem can be expressed by a Boolean combination of arithmetic constraints and ordinary differential equations (ODEs). While the Boolean, integer, and realvalued variables represent the state of the hybrid system, the constraint system describes traces characterized by their initial states, a transition relation connecting subsequent states by continuous flows or discrete jumps, and a target state whose reachability is to be analyzed. The reachability problem of the hybrid system therefore becomes a satisfiability problem of this type of formula. We extend our constraint solving algorithm iSAT to also handle the ODEs occuring in these formulae by using safe enclosures of the ODEs solution trajectories thereby coupling the structure of the DPLL procedure, which is used successfully in propositional satisfiability solving, with interval methods for arithmetic constraints and safe enclosure methods for the solutions of initial value problems. Our current work is focused (1) on exchanging our prototypical enclosure mechanism with Ned Nedialkov's VNODELP in order to obtain such enclosures more efficiently and (2) on storing oncededuced knowledge and potentially further information available on the solution trajectories persistently in the constraint system to avoid costly enclosures in the first place. Keywords: Hybrid discrete continuous systems, automatic verification, satisfiability modulo theories, ordinary differential equations Joint work of: Eggers, Andreas; Fraenzle, Martin; Herde, Christian} } 
[phdthesis] bibtexC. Herde, "Efficient Solving of Large Arithmetic Constraint Systems with Complex Boolean Structure: Proof Engines for the Analysis of Hybrid DiscreteContinuous Systems," PhD Thesis , 2010.
@PhdThesis{Herde:Thesis,
author = "Christian Herde", title = "Efficient Solving of Large Arithmetic Constraint Systems with Complex Boolean Structure: Proof Engines for the Analysis of Hybrid DiscreteContinuous Systems", school = "Carl von Ossietzky Universi{\"a}t Oldenburg", year = "2010", type = "Doctoral Dissertation", subproject = {H1/2},
access = {restricted},
bibtex = {herde.phd.2010.bib},
abstract = "Due to the increasing use of more and more complex computerized systems in safetycritical applications, formal verification of such systems is of growing importance. Among the most successful methods in formal verification of finitestate systems is bounded model checking (BMC), a technique for checking whether an unsafe system state is reachable within a fixed number of steps. BMC belongs to a class of verification algorithms having in common that the verification task is reduced to the problem of checking the satisfiability of a propositional formula or a series thereof. Though originally formulated for discrete transition systems only, BMC is in principle also applicable to hybrid discretecontinuous systems, which naturally arise e.g. in the field of embedded systems where digital (discrete) controllers are coupled with analog (continuous) physical plants. The BMC formulae arising from such systems are, however, no longer purely propositional, but usually comprise complex Boolean combinations of arithmetic constraints over realvalued variables, thus entailing the need for new decision procedures to solve them. This thesis deals with the development of such procedures. A key component of the algorithms we present is the DPLL procedure for solving Boolean formulae which are in conjunctive normal form (CNF). As a first contribution, we demonstrate that the acceleration techniques, which enabled the enormous performance gains of Boolean SAT solvers in the recent past, generalize smoothly to DPLLbased procedures for solving systems of pseudoBoolean constraints, a much more concise representation of Boolean functions than CNFs. Second, we investigate how to efficiently couple a linear programming routine with a DPLLbased SAT solver in order to obtain a solver which is tailored for BMC of hybrid systems with linear dynamics. In particular, we examine how to exploit the unique characteristics of BMC formulae and the incremental nature of BMC for various optimizations inside the solver. Finally, we present our main contribution, a tight integration of the DPLL procedure with interval constraint solving, resulting in an algorithm, called iSAT, which generalizes the DPLL procedure and is capable of solving arbitrary Boolean combinations of nonlinear arithmetic constraints over the reals, even such involving transcendental functions. We demonstrate the applicability of our methods using benchmarks from the envisaged application domain.", } 
[inproceedings] bibtexE. Olderog und M. Swaminathan, "Layered Composition for Timed Automata," in Proc. 8th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2010), 2010, pp. 228242.
@INPROCEEDINGS{,
author = {Olderog, ErnstR{\"{u}}diger and Swaminathan, Mani},
month = sep, title = {Layered Composition for Timed Automata},
booktitle = {8th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2010)},
series = {Lecture Notes in Computer Science},
volume = {6246},
year = {2010},
pages = {228242},
publisher = {Springer},
location = {Klosterneuburg, Austria},
isbn = {9783642152962},
doi = {http://dx.doi.org/10.1007/9783642152979_18},
abstract = {We investigate layered composition for realtime systems modelled as (networks of) timed automata (TA). We first formulate the principles of layering and transition independence for TA, and demonstrate the validity of the communication closed layer (CCL) laws in such a setting, by means of an operator for layered composition that is intermediate between parallel and sequential composition. Next, we introduce the principles of input/output (i/o) and partialorder (po) equivalences, and show that such equivalences are preserved when the layered composition operator is replaced by sequential composition within the expressions appearing in the CCL laws. Finally, we proceed to show that such layering (together with equivalences obtained through the CCL laws) can be useful in the design and verification of dense realtime systems that consist of a network of interacting components, by bringing about a reduction of the statespace through the exploitation of transition independence. This is illustrated by considering a collision avoidance protocol developed for an audio/video system of Bang and Olufsen.} }
2009

[inproceedings] bibtexT. Teige, "Stochastic Satisfiability Modulo Theories: A Technique for the Analysis of Probabilistic Hybrid Systems," in Proc. Dagstuhl 2009  Proceedings des gemeinsamen Workshops der InformatikGraduiertenkollegs und Forschungskollegs, 2009, pp. 5253.
@InProceedings{TeigeDagstuhl09:SSMT,
author = {Tino Teige},
title = {{Stochastic Satisfiability Modulo Theories: A Technique for the Analysis of Probabilistic Hybrid Systems}},
booktitle = {Dagstuhl 2009  Proceedings des gemeinsamen Workshops der InformatikGraduiertenkollegs und Forschungskollegs},
editor = {Artin Avanes and Dirk Fahland and Joanna Geibig and Siamak Haschemi and Sebastian Heglmeier and Daniel A. Sadile and Falko Theisselmann and Guido Wachsmuth and Stephan Wei{\ss}leder},
year = {2009},
pages = {5253},
publisher = {Gito Verlag},
note = {ISBN: 9783940019738} } 
[inproceedings] bibtexT. Teige und M. Fränzle, "ConstraintBased Analysis of Probabilistic Hybrid Systems," in Proc. Proceedings of the 3rd IFAC Conference on Analysis and Design of Hybrid Systems (ADHS 2009), 2009, pp. 162167.
@InProceedings{TeigeFraenzle09:ADHS,
author = {Tino Teige and Martin Fr{\"a}nzle},
title = {{ConstraintBased Analysis of Probabilistic Hybrid Systems}},
booktitle = {Proceedings of the 3rd IFAC Conference on Analysis and Design of Hybrid Systems (ADHS 2009)},
publisher = {IFAC},
editor = {A. Giua and C. Mahulea and M. Silva and J. Zaytoon},
pages = {162167},
year = {2009} } 
[inproceedings] bibtexS. Kupferschmid, T. Teige, B. Becker, und M. Fränzle, "Proofs of Unsatisfiability for mixed Boolean and Nonlinear Arithmetic Constraint Formulae," in Proc. Proceedings of the 12th Workshop ``Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen'' (MBMV 2009), 2009, pp. 2736.
@InProceedings{KupferschmidEtAl09:MBMV,
author = {Stefan Kupferschmid and Tino Teige and Bernd Becker and Martin Fr{\"a}nzle},
title = {{Proofs of Unsatisfiability for mixed Boolean and Nonlinear Arithmetic Constraint Formulae}},
booktitle = {Proceedings of the 12th Workshop ``Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen'' (MBMV 2009)},
editor = {Carsten Gremzow and Nico Moser},
pages = {2736},
year = {2009},
publisher = {Universit{\"a}tsverlag TU Berlin},
isbn = {9783798321182} } 
[inproceedings] bibtex  Dokument aufrufenA. Eggers, N. Kalinnik, S. Kupferschmid, und T. Teige, "Challenges in ConstraintBased Analysis of Hybrid Systems," in Proc. Recent Advances in Constraints  13th Annual ERCIM International Workshop on Constraint Solving and Constraint Logic Programming, CSCLP 2008, Rome, Italy, June 1820, 2008, Revised Selected Papers, Berlin, Heidelberg, 2009, pp. 5165.
@InProceedings{EggKalKupTei:RAC08:Challenges,
author = "Andreas Eggers and Natalia Kalinnik and Stefan Kupferschmid and Tino Teige", title = "Challenges in ConstraintBased Analysis of Hybrid Systems", booktitle = "Recent Advances in Constraints  13th Annual ERCIM International Workshop on Constraint Solving and Constraint Logic Programming, CSCLP 2008, Rome, Italy, June 1820, 2008, Revised Selected Papers", editor = "Angelo Oddi and Fran\c{c}ois Fages and Francesca Rossi", publisher = "Springer", address = "Berlin, Heidelberg", series = "Lecture Notes in Artificial Intelligence", volume = "5655", pages = "5165", year = "2009", doi = "10.1007/9783642032516_4", url = "http://dx.doi.org/10.1007/9783642032516_4", note = "Springerlink: \url{http://www.springerlink.com/content/hx755817464v6746}", subproject= {H1/2},
abstract = "In the analysis of hybrid discretecontinuous systems, rich arithmetic constraint formulae with complex Boolean structure arise naturally. The iSAT algorithm, a solver for such formulae, is aimed at bounded model checking of hybrid systems. In this paper, we identify challenges emerging from planned and ongoing work to enhance the iSAT algorithm. First, we propose an extension of iSAT to directly handle ordinary differential equations as constraints. Second, we outline the recently introduced generalization of the iSAT algorithm to deal with probabilistic hybrid systems and some open research issues in that context. Third, we present ideas on how to move from bounded to unbounded model checking by using the concept of interpolation. Finally, we discuss the adaption of some parallelization techniques to the iSAT case, which will hopefully lead to performance gains in the future. By presenting these open research questions, this paper aims at fostering discussions on these extensions of constraint solving.", keywords = "mixed Boolean and arithmetic constraints  differential equations  stochastic SMT  Craig interpolation  parallel solver " } 
[inproceedings] bibtex  Dokument aufrufenA. Eggers, M. Fränzle, und C. Herde, "Application of Constraint Solving and ODEEnclosure Methods to the Analysis of Hybrid Systems," in Proc. NUMERICAL ANALYSIS AND APPLIED MATHEMATICS: International Conference on Numerical Analysis and Applied Mathematics 2009, Melville, New York, 2009, pp. 13261330.
@InProceedings{EggFraHer:ICNAAM09:ApplicationConstraintSolvingODEHybridSystems,
author = "Andreas Eggers and Martin Fr{\"a}nzle and Christian Herde", title = "Application of Constraint Solving and ODEEnclosure Methods to the Analysis of Hybrid Systems", booktitle = "NUMERICAL ANALYSIS AND APPLIED MATHEMATICS: International Conference on Numerical Analysis and Applied Mathematics 2009", editor = "Theodore E. Simos and George Psihoyios and Ch. Tsitouras", publisher = "American Institute of Physics", address = "Melville, New York", series = "AIP Conference Proceedings", volume = "1168", pages = "13261330", year = "2009", url = "http://link.aip.org/link/?APC/1168/1326/1", doi = "10.1063/1.3241327", subproject= "H1/2", abstract = "In this short paper, we summarize our approach to analyzing hybrid discretecontinuous systems by reduction to constraint solving paired with enclosure methods for sets of initial value problems of ordinary differential equations.", keywords = "hybrid discretecontinuous systems, verification, ordinary differential equations, constraint solving, PACS: 02.60.Lj, 02.70.c, 89.75.k" } 
[inproceedings] bibtex  Dokument aufrufenG. Sauter, H. Dierks, M. Fränzle, und M. R. Hansen, "Lightweight hybrid model checking facilitating online prediction of temporal properties," in Proc. Proceedings of the 21st Nordic Workshop on Programming Theory, NWPT '09, Kgs. Lyngby, Denmark, 2009, pp. 2022.
@INPROCEEDINGS{SauterEA:NWPT09,
author = {Gerald Sauter and Henning Dierks and Martin Fr{\"a}nzle and Michael R. Hansen},
title = {Lightweight hybrid model checking facilitating online prediction of temporal properties},
booktitle = {Proceedings of the 21st Nordic Workshop on Programming Theory, NWPT '09},
year = {2009},
pages = {2022},
address = {Kgs. Lyngby, Denmark},
note = {\url{http://imost.informatik.unioldenburg.de}},
url = {http://imost.informatik.unioldenburg.de/download/RobustMonitoringNWPT09.pdf},
publisher = {Danmarks Tekniske Universitet} } 
[techreport] bibtex  Dokument aufrufenG. Sauter, H. Dierks, M. Fränzle, und M. R. Hansen, "Lightweight hybrid model checking facilitating online prediction of temporal properties," Carl von Ossietzky Universität Oldenburg2009.
@TECHREPORT{SauterEA:TechReport,
author = {Gerald Sauter and Henning Dierks and Martin Fr{\"a}nzle and Michael R. Hansen},
title = {Lightweight hybrid model checking facilitating online prediction of temporal properties},
institution = {Carl von Ossietzky Universit{\"a}t Oldenburg},
year = {2009},
note = {\url{http://imost.informatik.unioldenburg.de}},
url = {http://imost.informatik.unioldenburg.de/download/TecReport_IMoST_001.pdf},
abstract = {We address the problem of online prediction of future temporal properties of open continuous systems based on time series obtained from online measurements. The objective is, given a partial time series stating (possibly inexact) measurements of observable variables of the system, to safely predict the truth value of a lineartime temporallogic formula including future modalities, and to do so in realtime while the system is evolving. While this can in principle be done using techniques from hybridsystem model checking, these algorithms are computationally by far too expensive to support online prediction in realtime. As a computationally tractable alternative, we suggest an approach decomposing hybrid modelchecking into an offline and an online phase, where the offline phase precomputes all computationally expensive entities, in particular those involving forms of branching, while the online part exploits these precomputed properties in a branchingfree analysis based on computationally inexpensive interval constraint propagation. The procedure is designed for systemintheloop testing or similar use cases requiring realtime monitoring of dynamic processes with respect to temporal properties at moderately high sampling frequencies.} } 
[inproceedings] bibtex  Dokument aufrufenM. Fränzle und M. Swaminathan, "Revisiting Decidability and Optimum Reachability for MultiPriced Timed Automata," in Proc. The 7th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS 2009), 2009, pp. 149163.
@InProceedings{SwaminathanFraenzleFORMATS09,
author = {Martin Fr{\"a}nzle and Mani Swaminathan},
title = {Revisiting Decidability and Optimum Reachability for MultiPriced Timed Automata},
booktitle = {The 7th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS 2009)},
editor = {J. Ouaknine and F. Vaandrager},
pages = {149163},
year = {2009},
month = {September},
publisher = {Springer Verlag},
url = {http://dx.doi.org/10.1007/9783642043680_13} } 
[inproceedings] bibtexM. Fränzle, "Engineering constraint solvers for the analysis of hybrid systems," in Proc. 20th Nordic Workshop on Programming Theory, NWPT '08, 2008, p. 9.
@INPROCEEDINGS{Fraenzle:NWPT08,
author = "Martin Fr{\"a}nzle", title = "Engineering constraint solvers for the analysis of hybrid systems", booktitle = "20th Nordic Workshop on Programming Theory, NWPT '08", editors = "Tarmo Uustalu and J{\"u}ri Vain and Juhan Ernits", pages = "9", publisher = "Institute of Cybernetics, Tallinn Technical University", year = "2008"} 
[inproceedings] bibtexM. Fränzle, A. Eggers, C. Herde, und T. Teige, "Hybrid DiscreteContinuous Systems," in Proc. Modern Computational Science 09, 2009, pp. 363378.
@InProceedings{FraenzleEA:MCS,
author = "Martin Fr{\"a}nzle and Andreas Eggers and Christian Herde and Tino Teige", title = "Hybrid DiscreteContinuous Systems", booktitle = "Modern Computational Science 09", editors = "Reinhard Leidl and Hartmann, Alexander K.", publisher = "BISVerlag der Carl von Ossietzky Universit{\"a}t Oldenburg", year = "2009", pages = "363378"} 
[inproceedings] bibtexW. P. Heise, M. R. Hansen, und M. Fränzle, "A prototype of a model checker for Duration Calculus," in Proc. Proceedings of the 21st Nordic Workshop on Programming Theory, NWPT '09, Kgs. Lyngby, Denmark, 2009, pp. 2628.
@INPROCEEDINGS{WilliamEA:BranchingDCNWPT,
author = {Heise, William Pihl and Hansen, Michael R. and Martin Fr{\"a}nzle},
title = {A prototype of a model checker for Duration Calculus},
booktitle = {Proceedings of the 21st Nordic Workshop on Programming Theory, NWPT '09},
year = {2009},
address = {Kgs. Lyngby, Denmark},
publisher = {DTU Informatics, Danmarks Tekniske Universitet},
pages = {2628} } 
[article] bibtexM. Fränzle und M. R. Hansen, "Efficient Model Checking for Duration Calculus," International Journal of Software and Informatics, vol. 3, iss. 23, pp. 171196, 2009.
@Article{FraenzleHansen:BranchingTimeDCJournal,
author = {Martin Fr{\"a}nzle and Hansen, Michael R.},
title = {Efficient Model Checking for Duration Calculus},
journal = {International Journal of Software and Informatics},
volume = "3", number = "23", pages = "171196", year = {2009} } 
[inproceedings] bibtexJ. Gacnic, H. Jost, F. Köster, J. Rataj, K. Lemmer, W. Damm, M. Fränzle, und E. Schnieder, "DeSCAS  Formale Ontologien zur Verwebung von interdisziplinären Entwicklungsprozessen," in Proc. AUTOMATION 2009  Der Automatisierungskongress in Deutschland, Düsseldorf, 2009, pp. 449453.
@inproceedings{GacnicEtAl,
author = {Jan Gacnic and Henning Jost and Frank K{\"o}ster and J{\"u}rgen Rataj and Karsten Lemmer and Werner Damm and Martin Fr{\"a}nzle and Eckehard Schnieder},
title = {{DeSCAS}  Formale Ontologien zur Verwebung von interdisziplin{\"a}ren Entwicklungsprozessen},
year = 2009, month = 6, publisher = {VDI Verlag},
address = {D{\"u}sseldorf},
booktitle = {{AUTOMATION} 2009  Der Automatisierungskongress in Deutschland},
series = {VDIBerichte/VDITagungsb{\"a}nde},
number = {2067},
issn = {00835560},
isbn = {9783180920672},
pages = {449453},
note = {Umfang der beigef. CDROM Version: 12 Seiten} }
2008

[techreport] bibtexT. Teige, C. Herde, M. Fränzle, und E. Ábrahám, "Conflict Analysis and Restarts in a mixed Boolean and Nonlinear Arithmetic Constraint Solver," SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 34, with 12 pages, 2008.
@techreport{atr34,
author = {Tino Teige and Christian Herde and Martin Fr{\"a}nzle and Erika \'Abrah\'am},
title = {{Conflict Analysis and Restarts in a mixed Boolean and Nonlinear Arithmetic Constraint Solver}},
editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski and Reinhard Wilhelm},
institution = {SFB/TR 14 AVACS},
subproject = {H1/2},
year = {2008},
month = {January},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
number = {34, with 12 pages},
note = {ISSN: 18609821, http://www.avacs.org.},
access = {open},
abstract = { The recently presented constraint solver HySAT tackles the in general undecidable problem of solving mixed Boolean and nonlinear arithmetic constraint formulae over the reals involving transcendental functions. The algorithmic core of HySAT is the iSAT algorithm, a tight integration of the DavisPutnamLogemannLoveland algorithm with interval constraint propagation enriched by enhancements like conflictdriven clause learning and nonchronological backtracking. However, it was an open question whether HySAT's conflict analysis scheme, an adapted first unique implication point technique as applied in most modern SAT solvers, performs favorably compared to other schemes. In this paper, we compare several conflict analysis heuristics to answer this question. Furthermore, we consider the integration of restarts into the iSAT algorithm and investigate their impact. For our empirical results we use benchmarks from the hybrid systems domain.},
bibtex = {atr034.bib},
pdf = {avacs_technical_report_034.pdf} } 
[techreport] bibtexS. Kupferschmid, T. Teige, B. Becker, und M. Fränzle, "Proofs of Unsatisfiability for mixed Boolean and Nonlinear Arithmetic Constraint Formulae," SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 40, with 13 pages, 2008.
@techreport{atr40,
author = {Stefan Kupferschmid and Tino Teige and Bernd Becker and Martin Fr{\"a}nzle},
title = {{Proofs of Unsatisfiability for mixed Boolean and Nonlinear Arithmetic Constraint Formulae}},
editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski and Reinhard Wilhelm},
institution = {SFB/TR 14 AVACS},
subproject = {H1/2},
year = {2008},
month = {June},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
number = {40, with 13 pages},
note = {ISSN: 18609821, http://www.avacs.org.},
access = {open},
abstract = { In recent years, the use of constraint solvers for analysis and verification of industrial systems has become increasingly popular. The correctness and reliability of the results returned by the employed solvers are a vital requirement, in particular for safetycritical systems. If a solver proves the satisfiability of a constraint system and returns a solution then the answer of the solver can be validated by means of the solution. However, in case the solver claims that the constraint system is unsatisfiable without any certificate then the validation of this answer is not that simple. In this paper, we establish the theoretical basis of generating proofs of unsatisfiability in the mixed Boolean and nonlinear arithmetic constraint framework over the reals and integers. To do so, we propose a simple rulebased calculus for unsatisfiable mixed Booleanarithmetic constraints to produce and check unsatisfiability proofs. Furthermore, we enhance the iSAT constraint solver to generate unsatisfiability proofs, we implement a tool validating such proofs, and give some experimental results.},
bibtex = {atr040.bib},
pdf = {avacs_technical_report_040.pdf} } 
[inproceedings] bibtexA. Eggers, N. Kalinnik, S. Kupferschmid, und T. Teige, "Challenges in Constraintbased Analysis of Hybrid Systems," in Proc. Preproceedings of the Annual ERCIM Workshop on Constraint Solving and Constraint Logic Programming (CSCLP 2008), 2008, pp. 115.
@InProceedings{EggersEtAl08:Challenges,
author = {A. Eggers and N. Kalinnik and S. Kupferschmid and T. Teige},
title = {{Challenges in Constraintbased Analysis of Hybrid Systems}},
booktitle = {Preproceedings of the Annual ERCIM Workshop on Constraint Solving and Constraint Logic Programming (CSCLP 2008)},
pages = {115},
year = {2008},
month = {June},
location = {Rome, Italy},
subproject = {H1/2},
access = {open},
note = {http://pst.istc.cnr.it/CSCLP08/program/papers/EggersEtalCSCLP2008.pdf},
bibtex = {eggers.csclp08.bib},
pdf = {eggers.csclp08.pdf},
abstract = { In the analysis of hybrid discretecontinuous systems, rich arithmetic constraint formulae with complex Boolean structure arise naturally. The iSAT algorithm, a solver for such formulae, is aimed at bounded model checking of hybrid systems. In this paper, we identify challenges emerging from planned and ongoing work to enhance the iSAT algorithm: First, we propose an extension of iSAT to directly handle ordinary differential equations as constraints. Second, we outline the recently introduced generalization of the iSAT algorithm to deal with probabilistic hybrid systems and some open research issues in that context. Third, we present ideas on how to move from bounded to unbounded model checking by using the concept of interpolation. Finally, we discuss the adaption of some parallelization techniques to the iSAT case, which will hopefully lead to performance gains in the future. By presenting these open research questions, this paper aims at fostering discussions on these extensions of constraint solving.} } 
[inproceedings] bibtexM. Fränzle, H. Hermanns, und T. Teige, "Stochastic Satisfiability Modulo Theory: A Novel Technique for the Analysis of Probabilistic Hybrid Systems," in Proc. PreProceedings of the ETAPS 2008 Sixth Workshop on Quantitative Aspects of Programming Languages (QAPL 2008), 2008, pp. 14.
@InProceedings{FraHerTei08:QAPL:SSMT,
author = {M. Fr{\"a}nzle and H. Hermanns and T. Teige},
title = {{Stochastic Satisfiability Modulo Theory: A Novel Technique for the Analysis of Probabilistic Hybrid Systems}},
booktitle = {PreProceedings of the ETAPS 2008 Sixth Workshop on Quantitative Aspects of Programming Languages (QAPL 2008)},
pages = {14},
year = {2008},
editor = {Alessandro Aldini and Christel Baier},
keywords = {Stochastic satisfiability, infinite domains, probabilistic hybrid automata, probabilistic bounded reachability.},
subproject = {H1/2,H4},
access = {open},
note = {http://www.avacs.org},
bibtex = {fraenzle.qapl08.bib},
pdf = {fraenzle.qapl08.pdf},
abstract = {The analysis of hybrid systems exhibiting probabilistic behaviour is notoriously difficult. To enable mechanised analysis of such systems, we extend the reasoning power of arithmetic satisfiabilitymodulotheory solving (SMT) by a comprehensive treatment of randomized (a.k.a. stochastic) quantification over discrete variables within the mixed Booleanarithmetic constraint system. This provides the technological basis for a fully symbolic analysis of probabilistic hybrid automata. Generalizing SMTbased bounded modelchecking of hybrid automata [2,9], stochastic SMT permits the direct and fully symbolic analysis of probabilistic bounded reachability problems of probabilistic hybrid automata without resorting to approximation by intermediate finitestate abstractions.} } 
[inproceedings] bibtexM. Fränzle, H. Hermanns, und T. Teige, "Stochastic Satisfiability Modulo Theory: A Novel Technique for the Analysis of Probabilistic Hybrid Systems," in Proc. Proceedings of the 11th International Conference on Hybrid Systems: Computation and Control (HSCC'08), 2008, pp. 172186.
@InProceedings{FraHerTei08:SSMT,
author = {M. Fr{\"a}nzle and H. Hermanns and T. Teige},
title = {{Stochastic Satisfiability Modulo Theory: A Novel Technique for the Analysis of Probabilistic Hybrid Systems}},
booktitle = {Proceedings of the 11th International Conference on Hybrid Systems: Computation and Control (HSCC'08)},
pages = {172186},
editor = {Magnus Egerstedt and Bud Mishra},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4981},
year = {2008},
note = {ISBN:9783540789284},
subproject = {H1/2,H4},
bibtex = {fraenzle.hscc08.bib},
pdf = {fraenzle.hscc08.pdf},
access = {restricted},
abstract = {The analysis of hybrid systems exhibiting probabilistic behaviour is notoriously difficult. To enable mechanised analysis of such systems, we extend the reasoning power of arithmetic satisfiabilitymodulotheory solving (SMT) by a comprehensive treatment of randomized (a.k.a. stochastic) quantification over discrete variables within the mixed Booleanarithmetic constraint system. This provides the technological basis for a fully symbolic analysis of probabilistic hybrid automata. Generalizing SMTbased bounded modelchecking of hybrid automata [2, 11], stochastic SMT permits the direct and fully symbolic analysis of probabilistic bounded reachability problems of probabilistic hybrid automata without resorting to approximation by intermediate finitestate abstractions.} } 
[inproceedings] bibtexT. Teige, "Stochastic Satisfiability Modulo Theory: A Technique for the Analysis of Probabilistic Hybrid Systems," in Proc. Proceedings des gemeinsamen Workshops der Graduiertenkollegs 2008, Dagstuhl, Berlin, 2008, pp. 3334.
@INPROCEEDINGS{TeigeDagstuhl08:SSMT,
author = {Tino Teige},
title = {{Stochastic Satisfiability Modulo Theory: A Technique for the Analysis of Probabilistic Hybrid Systems}},
booktitle = {Proceedings des gemeinsamen Workshops der Graduiertenkollegs 2008, Dagstuhl},
year = {2008},
editor = {Malte Diehl and Henrik Lipskoch and Roland Meyer and Christian Storm},
series = {Trustworthy Software Systems},
pages = {3334},
address = {Berlin},
month = {May},
publisher = {Gito Verlag},
note = {ISBN: 9783940019394},
location = {May 1921, 2008, Dagstuhl, Germany} } 
[inproceedings] bibtexT. Teige und M. Fränzle, "Stochastic Satisfiability modulo Theories for Nonlinear Arithmetic," in Proc. Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, 5th International Conference, CPAIOR 2008, 2008, pp. 248262.
@InProceedings{TeiFra08:nonlinearSSMT,
author = {T. Teige and M. Fr{\"a}nzle},
title = {{Stochastic Satisfiability modulo Theories for Nonlinear Arithmetic}},
booktitle = {Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, 5th International Conference, CPAIOR 2008},
editor = {L. Perron and M.~A. Trick},
year = {2008},
pages = {248262},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5015},
note = {ISBN: 9783540681540},
subproject = {H1/2,H4},
access = {restricted},
bibtex = {teige.cpaior08.bib},
pdf = {teige.cpaior08.pdf},
abstract = {The stochastic satisfiability modulo theories (SSMT) problem is a generalization of the SMT problem on existential and randomized (aka. stochastic) quantification over discrete variables of an SMT formula. This extension permits the concise description of diverse problems combining reasoning under uncertainty with data dependencies. Solving problems with various kinds of uncertainty has been extensively studied in Artificial Intelligence. Famous examples are stochastic satisfiability and stochastic constraint programming. In this paper, we extend the algorithm for SSMT for decidable theories presented in [FHT08] to nonlinear arithmetic theories over the reals and integers which are in general undecidable. Therefore, we combine approaches from Constraint Programming, namely the iSAT algorithm tackling mixed Boolean and nonlinear arithmetic constraint systems, and from Artificial Intelligence handling existential and randomized quantifiers. Furthermore, we evaluate our novel algorithm and its enhancements on benchmarks from the probabilistic hybrid systems domain.} } 
[techreport] bibtexA. Eggers, M. Fränzle, und C. Herde, "SAT Modulo ODE: A Direct SAT approach to Hybrid Systems," SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 37 with 14 Pages, 2008.
@TECHREPORT{atr37,
author = {Andreas Eggers and Martin Fr{\"a}nzle and Christian Herde},
title = {{{SAT} Modulo {ODE}: A Direct {SAT} approach to Hybrid Systems}},
institution = {SFB/TR 14 AVACS},
year = {2008},
type = {Reports of SFB/TR 14 AVACS},
number = {37 with 14 Pages},
month = {April},
note = {ISSN: 18609821, http://www.avacs.org},
abstract = {In order to facilitate automated reasoning about large Boolean combinations of nonlinear arithmetic constraints involving ordinary differential equations (ODEs), we provide a seamless integration of safe numeric overapproximation of initialvalue problems into a SATmodulotheory (SMT) approach to intervalbased arithmetic constraint solving. Intervalbased safe numeric approximation of ODEs is used as an interval contractor being able to narrow candidate sets in phase space in both temporal directions: postimages of ODEs (i.e., sets of states reachable from a set of initial values) are narrowed based on partial information about the initial values and, vice versa, preimages are narrowed based on partial knowledge about postsets. In contrast to the related CLP(F) approach of Hickey and Wittenberg, we do (a) support coordinate transformations mitigating the wrapping effect encountered upon iterating intervalbased overapproximations of reachable state sets and (b) embed the approach into an SMT framework, thus accelerating the solving process through the algorithmic enhacements of recent SAT solving technology. },
access = {open},
bibtex = {atr037.bib},
pdf = {avacs_technical_report_037.pdf},
editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski and Reinhard Wilhelm},
series = {ATR},
subproject = {H1/2} } 
[inproceedings] bibtexA. Eggers, M. Fränzle, und C. Herde, "SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems," in Proc. Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis (ATVA'08), 2008, pp. 171185.
@inproceedings{EggFraHer:ATVA08:SATmodODE,
author = {Andreas Eggers and Martin Fr{\"a}nzle and Christian Herde},
title = {{SAT} Modulo {ODE}: A Direct {SAT} Approach to Hybrid Systems},
booktitle = {Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis (ATVA'08)},
year = {2008},
pages = {171185},
editor = {Sungdeok (Steve) Cha and JinYoung Choi and Moonzoo Kim and Insup Lee and Mahesh Viswanathan},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5311},
note = {ISBN: 9783540883869},
subproject = {H1/2},
bibtex = {eggers.atva08.bib},
pdf = {eggers.atva08.pdf},
access = {restricted},
abstract = {In order to facilitate automated reasoning about large Boolean combinations of nonlinear arithmetic constraints involving ordinary differential equations (ODEs), we provide a seamless integration of safe numeric overapproximation of initialvalue problems into a SATmodulotheory (SMT) approach to intervalbased arithmetic constraint solving. Intervalbased safe numeric approximation of ODEs is used as an interval contractor being able to narrow candidate sets in phase space in both temporal directions: postimages of ODEs (i.e., sets of states reachable from a set of initial values) are narrowed based on partial information about the initial values and, vice versa, preimages are narrowed based on partial knowledge about postsets. In contrast to the related CLP(F) approach of Hickey and Wittenberg, we do (a) support coordinate transformations mitigating the wrapping effect encountered upon iterating intervalbased overapproximations of reachable state sets and (b) embed the approach into an SMT framework, thus accelerating the solving process through the algorithmic enhancements of recent SAT solving technology.} } 
[inproceedings] bibtexC. Herde, A. Eggers, M. Fränzle, und T. Teige, "Analysis of Hybrid Systems using HySAT," in Proc. The Third International Conference on Systems (ICONS 2008), 2008, pp. 196201.
@InProceedings{HerEggFraTei08:HySAT,
author = {C. Herde and A. Eggers and M. Fr{\"a}nzle and T. Teige},
title = {{Analysis of Hybrid Systems using {HySAT}}},
booktitle = {The Third International Conference on Systems (ICONS 2008)},
publisher = {IEEE Computer Society},
year = {2008},
pages = {196201},
note = {ISBN: 9780769531052},
access = {restricted},
subproject = {H1/2},
bibtex = {herde.icons08.bib},
pdf = {herde.icons08.pdf},
abstract = {In this paper we describe the complete workflow of analyzing the dynamic behavior of safetycritical embedded systems with HySAT. HySAT is an arithmetic constraint solver with a tightly integrated bounded model checker for hybrid discretecontinuous systems which  in contrast to many other solvers  is not confined to linear arithmetic, but can also deal with nonlinear constraints involving transcendental functions. Based on a controller for train separation implementing a "moving block" interlocking scheme in the forthcoming European Train Control System Level 3, we exemplify the usage of the tool over the whole cycle from encoding a hybrid system to interpreting the results.} } 
[inproceedings] bibtex  Dokument aufrufenM. Swaminathan, M. Fränzle, und J. Katoen, "The Surprising Robustness of (Closed) Timed Automata against ClockDrift.," in Proc. Fifth IFIP International Conference on Theoretical Computer Science, 20080915 2008, pp. 537553.
@inproceedings{conf/ifipTCS/SwaminathanFK08, title = {{The Surprising Robustness of (Closed) Timed Automata against ClockDrift.}},
author = {Mani Swaminathan and Martin Fr\"anzle and JoostPieter Katoen},
booktitle = {Fifth IFIP International Conference on Theoretical Computer Science},
editor = {Giorgio Ausiello and Juhani Karhumki and Giancarlo Mauri and C.H. Luke Ong},
pages = {537553},
publisher = {Springer},
series = {IFIP International Federation for Information Processing},
url = {http://dblp.unitrier.de/db/conf/ifipTCS/ifipTCS2008.html#SwaminathanFK08},
volume = {273},
year = {2008},
biburl = {http://www.bibsonomy.org/bibtex/298ace7a31631e78231d29048d947dadd/dblp},
description = {dblp},
date = {20080915},
ee = {http://dx.doi.org/10.1007/9780387096803_36},
note = {ISBN: 9780387096797},
keywords = {dblp } } 
[inproceedings] bibtexM. Fränzle und M. R. Hansen, "Efficient Model Checking for Duration Calculus Based on BranchingTime Approximations," in Proc. 6th IEEE International Conferences on Software Engineering and Formal Methods, 2008, pp. 6372.
@InProceedings{FraenzleHansen08,
author = {Fr\"anzle, Martin and Hansen, Michael R.},
title = {{Efficient Model Checking for Duration Calculus Based on BranchingTime Approximations}},
booktitle = {6th IEEE International Conferences on Software Engineering and Formal Methods},
pages = {6372},
year = {2008},
month = {November},
publisher = {IEEE Computer Society Press},
note = {ISBN: 9780769534374},
subproject = {R1},
access = {restricted},
bibtex = {fraenzle.sefm08.bib},
pdf = {fraenzle.sefm08.pdf},
abstract = {Duration Calculus (abbreviated to DC) is an intervalbased, metrictime temporal logic designed for reasoning about embedded realtime systems at a high level of abstraction. But the complexity of model checking any decidable fragment featuring both negation and chop, DC's only modality, is nonelementary and thus impractical. We here investigate a similar approximation as frequently employed in model checking situationbased temporal logics, where lineartime problems are safely approximated by branchingtime counterparts amenable to more efficient modelchecking algorithms. Mimicking the role that a situation has in (A)CTL as origin of a set of linear traces, we define a branchingtime counterpart to intervalbased temporal logics building on situation pairs spanning sets of intervals. While this branchingtime interval semantics yields the desired reduction in complexity of the modelchecking problem, from nonelementary to linear in the size of the formula and cubic in the size of the model, the approximation is too coarse to be practical. We therefore refine the semantics by an occurrence count for crucial states (e.g., cuts of loops) in the model, arriving at a 4fold exponential modelchecking problem sufficiently accurately approximating the original one.},
} 
[inproceedings] bibtexM. Baumann, H. Colonius, H. Hungar, F. Köster, M. Langner, A. Lüdtke, C. Möbus, J. Peinke, S. Puch, C. Schiessl, R. Steenken, und L. Weber, "Integrated Modeling for Safe Transportation  Driver modeling and driver experiments.," in Proc. Fahrermodellierung in Wissenschaft und Wirtschaft, 2. Berliner Fachtagung für Fahrermodellierung, 2008.
@INPROCEEDINGS {baumann_et_al_a08,
author = {Baumann, M. and Colonius, H. and Hungar, H. and K\"oster, F. and Langner, M. and L\"udtke, A. and M\"obus, C. and Peinke, J. and Puch, S. and Schiessl, C. and Steenken, R. and Weber, L. },
BOOKTITLE = {Fahrermodellierung in Wissenschaft und Wirtschaft, 2. Berliner Fachtagung f\"ur Fahrermodellierung},
EDITOR = {J\"urgensohn and Kolrep},
PUBLISHER = {VDI Verlag},
SERIES = {Fortschrittsbericht des VDI in der Reihe 22 (MenschMaschineSysteme)},
TITLE = {Integrated Modeling for Safe Transportation  Driver modeling and driver experiments. },
YEAR = {2008} }
2007

[article] bibtexB. Badban, J. van de Pol, O. Tveretina, und H. Zantema, "Generalizing DPLL and Satisfiability for Equalities," Journal of Information and Computation, vol. 205, iss. 8, pp. 11881211, 2007.
@Article{bad07,
author = "Bahareh Badban and Jaco van de Pol and Olga Tveretina and Hans Zantema", title = "Generalizing {DPLL} and Satisfiability for Equalities", year = "2007", journal = "Journal of Information and Computation", volume = {205},
number = {8},
year = {2007},
issn = {08905401},
pages = {11881211},
doi = {http://dx.doi.org/10.1016/j.ic.2007.03.003},
publisher = {Academic Press, Inc.},
address = {Duluth, MN, USA},
keywords = "satisfiability, DPLL procedure, equality, ground term algebra, inductive datatypes, decision procedure", } 
[article] bibtexB. Becker, W. Damm, M. Fränzle, E. Olderog, A. Podelski, und R. Wilhelm, "SFB/TR 14 AVACS  Automatic Verification and Analysis of Complex Systems," it  Information Technology, vol. 49, iss. 2, pp. 118126, 2007.
@article{it2007,
author = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski and Reinhard Wilhelm},
title = {{SFB/TR 14 AVACS}  Automatic Verification and Analysis of Complex Systems},
journal= {it  Information Technology},
volume = {49},
year = {2007},
number = {2},
pages = {118126},
publisher={Oldenbourg Wissenschaftsverlag},
address= {M{\"u}nchen, Germany},
note = {http://itInformationTechnology.de, DOI 10.1524/itit.2007.49.2.118},
} 
[inproceedings] bibtexT. Teige, C. Herde, M. Fränzle, N. Kalinnik, und A. Eggers, "A Generalized Twowatchedliteral Scheme in a mixed Boolean and Nonlinear Arithmetic Constraint Solver," in Proc. Proceedings of the $13^th$ Portuguese Conference on Artificial Intelligence (EPIA 2007), 2007, pp. 729741.
@inproceedings{TeigeEtAl2WAS,
author = {Tino Teige and Christian Herde and Martin Fr\"anzle and Natalia Kalinnik and Andreas Eggers},
title = {A Generalized Twowatchedliteral Scheme in a mixed Boolean and Nonlinear Arithmetic Constraint Solver},
booktitle = {Proceedings of the $13^{th}$ Portuguese Conference on Artificial Intelligence (EPIA 2007)},
series = {New Trends in Artificial Intelligence},
editor = {Jos{\'e} Neves and Manuel Filipe Santos and Jos{\'e} Manuel Machado},
publisher = {APPIA},
year = {2007},
month = {December},
location = {Guimar\~{a}es, Portugal},
pages = {729741},
subproject = {H1, H2},
access={restricted},
bibtex={teige.epia07.bib},
pdf={teige.epia07.pdf},
abstract = {In its combination with conflictdriven clause learning the twowatchedliteral scheme led to enormous performance gains in propositional SAT solving. The idea of this approach is to accelerate the deduction phase of a SAT solver by saving a high number of unnecessary and expensive computation steps originating in visits of indefinite clauses. In this paper we give a detailed explanation of the generalized watch scheme, called \emph{twowatchedatom scheme},
implemented in our intervalbased constraint solver HySAT, the latter being a solver for mixed Boolean and nonlinear arithmetic constraint formulae. As opposed to the purely Boolean setting, the more general form of atomic formulae to be watched in our solver necessitates an extension of the original scheme and calls for a careful design of the data structures employed in the implementation. We present experimental results to demonstrate the speedup obtained by the proposed scheme.},
} 
[inproceedings] bibtexM. Swaminathan und M. Fränzle, "A Symbolic Decision Procedure for Robust Safety of Timed Systems," in Proc. proceedings on the 14th International Symposium on Temporal Representation and Reasoning (TIME 2007), 2007.
@INPROCEEDINGS{swaminathan07,
author={Mani Swaminathan and Martin Fr{\"a}nzle},
title={A Symbolic Decision Procedure for Robust Safety of Timed Systems},
note={To appear as a short paper/poster},
booktitle={proceedings on the 14th International Symposium on Temporal Representation and Reasoning (TIME 2007)},
publisher={IEEE CS Press},
year={2007},
subproject={H1},
access={restricted},
bibtex={swaminathan.time07.bib},
pdf={swaminathan.time07.pdf},
abstract={We present a symbolic algorithm for deciding safety (reachability) of timed systems modelled as Timed Automata (TA), under the notion of robustness w.r.t infinitesimal clockdrift. The algorithm uses a ``neighbourhood'' operator on zones that is efficient to compute. In contrast to other approaches for robustly deciding reachability of TA, which are either regionbased (Puri, 2000), (DeWulf, Doyen, Markey, and Raskin, 2004), or involve a combination of forward and backward analyses when zonebased (Daws and Kordy, 2006), ours is a zonebased fully forward algorithm that is guaranteed to terminate, requires no special treatment of cycles in TA, and can be applied to target states that need not be closed.},
} 
[inproceedings] bibtexM. Fränzle und M. R. Hansen, "Deciding an Interval Logic with Accumulated Durations," in Proc. Thirteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 07), 2007, pp. 201215.
@InProceedings{FraenzleHansen:TACAS07,
author = {Fr{\"a}nzle, Martin and Hansen, Michael R.},
title = {Deciding an Interval Logic with Accumulated Durations},
booktitle = {Thirteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 07)},
year = {2007},
editor = {Grumberg, Orna and Huth, Michael},
series = {Lecture Notes in Computer Science},
publisher = {SpringerVerlag},
volume = {4424},
pages = {201215},
keywords = {Realtime systems, metrictime temporal logic, decidability, modelchecking, multipriced timed automata},
subproject = {H1},
access = {restricted},
pdf = {fraenzle.tacas07.pdf},
bibtex = {fraenzle.tacas07.bib},
abstract = {A decidability result and a modelchecking procedure for a rich subset of Duration Calculus (DC) [19] is obtained through reductions to is obtained through reductions to Firstorder logic over the realclosed field and to MultiPriced Timed Automata (MPTA) [13]. In contrast to other reductions of fragments of DC to reachability problems in timed automata, the reductions do also cover constraints on positive linear combinations of accumulated durations. By being able to handle accumulated durations under chop as well as in arbitrary positive Boolean contexts, the procedures extend the results of Zhou et al. [22] on decidability of linear duration invariants to a much wider fragment of DC.},
} 
[inproceedings] bibtexT. Teige, "SATModuloTheory based Analysis of Probabilistic Hybrid Systems," in Proc. Proceedings of the Dagstuhl Graduate School Meeting 2007 ``Dagstuhl Zehn plus Eins'', Aachen, 2007, pp. 8687.
@InProceedings{Teige07:SSMT,
author = {T. Teige},
title = {{SATModuloTheory based Analysis of Probabilistic Hybrid Systems}},
booktitle = {{Proceedings of the Dagstuhl Graduate School Meeting 2007 ``Dagstuhl Zehn plus Eins''}},
address = {Aachen},
year = {2007},
pages = {8687},
publisher = {Verlag Mainz},
note = {{ISBN:} 3861308827},
} 
[article] bibtexM. Fränzle, C. Herde, S. Ratschan, T. Schubert, und T. Teige, "Efficient Solving of Large Nonlinear Arithmetic Constraint Systems with Complex Boolean Structure," JSAT Special Issue on Constraint Programming and SAT, vol. 1, pp. 209236, 2007.
@Article{FraenzleEA:iSAT:JSAT,
author = {Martin Fr{\"a}nzle and Christian Herde and Stefan Ratschan and Tobias Schubert and Tino Teige},
title = {Efficient Solving of Large Nonlinear Arithmetic Constraint Systems with Complex Boolean Structure},
editor = {Y. Hamadi and L. Bordeaux},
journal = {JSAT Special Issue on Constraint Programming and SAT},
volume = {1},
pages = {209236},
year = {2007},
note = {accepted for publication},
subproject = {H1,H2},
access={restricted},
bibtex={fraenzle.jsat07.bib},
pdf={fraenzle.jsat07.pdf},
abstract={ In order to facilitate automated reasoning about large Boolean combinations of nonlinear arithmetic constraints involving transcendental functions, we provide a tight integration of recent SAT solving techniques with intervalbased arithmetic constraint solving. Our approach deviates substantially from lazy theorem proving approaches in that it directly controls arithmetic constraint propagation from the SAT solver rather than delegating arithmetic decisions to a subordinate solver. Through this tight integration, all the algorithmic enhancements that were instrumental to the enormous performance gains recently achieved in propositional SAT solving do smoothly carry over to the rich domain of nonlinear arithmetic constraints. As a consequence, our approach is able to handle large constraint systems with extremely complex Boolean structure, involving Boolean combinations of multiple thousand arithmetic constraints over some thousands of variables.},
} 
[article] bibtex  Dokument aufrufenM. Fränzle und C. Herde, "HySAT: An Efficient Proof Engine for Bounded Model Checking of Hybrid Systems," Formal Methods in System Design, vol. 30, pp. 179198, 2007.
@article{ FraenzleHerde05,
author = {Martin Fr{\"a}nzle and Christian Herde},
title = {{HySAT}: An Efficient Proof Engine for Bounded Model Checking of Hybrid Systems},
journal = {Formal Methods in System Design},
volume = 30, year = 2007, pages = {179198},
publisher = {SpringerVerlag Verlag},
keywords = {verification, bounded model checking, hybrid systems, infinitestate systems, decision procedures, satisfiability},
url = {http://dx.doi.org/10.1007/s1070300600310},
subproject = {H2},
language = {USenglish},
access = {restricted},
abstract = {In this paper we present HySAT, a new bounded model checker for linear hybrid systems, incorporating a tight integration of a DPLLbased pseudoBoolean SAT solver and a linear programming routine as core engine. In contrast to related tools like MathSAT, ICS, or CVC, our tool exploits all of the various optimizations that arise naturally in the bounded model checking context, e.g.~isomorphic replication of learned conflict clauses or tailored decision strategies, and extends them to the hybrid domain. We demonstrate that those optimizations are crucial to the performance of the tool.},
bibtex = {FMSD05_Fraenzle_Herde.bib},
pdf = {FMSD05_Fraenzle_Herde.pdf},
postscript = {FMSD05_Fraenzle_Herde.ps} } 
[techreport] bibtexT. Teige, C. Herde, M. Fränzle, und E. Ábrahám, "Conflict Analysis and Restarts in a mixed Boolean and Nonlinear Arithmetic Constraint Solver," SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 34, 2008.
@techreport{atr34,
author = {Tino Teige and Christian Herde and Martin Fr{\"a}nzle and Erika \'Abrah\'am},
title = {Conflict Analysis and Restarts in a mixed Boolean and Nonlinear Arithmetic Constraint Solver},
editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski and Reinhard Wilhelm},
institution = {SFB/TR 14 AVACS},
subproject = {H1/2},
year = {2008},
month = {January},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
number = 34, note = {ISSN: 18609821, http://www.avacs.org.},
access = {open},
abstract = { The recently presented constraint solver HySAT tackles the in general undecidable problem of solving mixed Boolean and nonlinear arithmetic constraint formulae over the reals involving transcendental functions. The algorithmic core of HySAT is the iSAT algorithm, a tight integration of the DavisPutnamLogemannLoveland algorithm with interval constraint propagation enriched by enhancements like conflictdriven clause learning and nonchronological backtracking. However, it was an open question whether HySAT's conflict analysis scheme, an adapted first unique implication point technique as applied in most modern SAT solvers, performs favorably compared to other schemes. In this paper, we compare several conflict analysis heuristics to answer this question. Furthermore, we consider the integration of restarts into the iSAT algorithm and investigate their impact. For our empirical results we use benchmarks from the hybrid systems domain.},
bibtex = {atr034.bib},
pdf = {avacs_technical_report_034.pdf} } 
[techreport] bibtexM. Fränzle, H. Hungar, C. Schmitt, und B. Wirtz, "HLang: Compositional Representation of Hybrid Systems via Predicates," SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 20, 2007.
@techreport{atr20,
author = {Martin Fr{\"a}nzle and Hardi Hungar and Christian Schmitt and Boris Wirtz},
title = {HLang: Compositional Representation of Hybrid Systems via Predicates},
editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski and Reinhard Wilhelm},
institution = {SFB/TR 14 AVACS},
subproject = {H1/2,H3},
year = {2007},
month = {July},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
number = 20, note = {ISSN: 18609821, http://www.avacs.org},
access = {open},
abstract = { Given the structural diversity of modeling paradigms for hybrid systems that are in widespread use, which ranges from a signaltransducerbased view like in Simulink/Stateflow to an automatonbased view in various hybrid automata frameworks, there is need for an intermediatelevel language that can accommodate these structures in a concise way, thereby isolating verification backends from the particular modeling frontend used. This technical report provides a description of the intermediatelevel modeling language for hybrid systems used in project area H of AVACS as a gateway to verification backends. },
bibtex = {atr020.bib},
pdf = {avacs_technical_report_020.pdf} } 
[inproceedings] bibtexE. Ábrahám, T. Schubert, B. Becker, M. Fränzle, und C. Herde, "Parallel SAT Solving in Bounded Model Checking," in Proc. Formal Methods: Applications and Technology, 11th International Workshop, FMICS 2006 and 5th International Workshop PDMC 2006, Bonn, Germany, August 2627, and August 31, 2006, Revised Selected Papers, 2007, pp. 301315.
@inproceedings{DBLP:conf/fmics/AbrahamSBFH06,
author = {Erika {\'A}brah{\'a}m and Tobias Schubert and Bernd Becker and Martin Fr{\"a}nzle and Christian Herde},
title = {Parallel SAT Solving in Bounded Model Checking},
editor = {Lubos Brim and Boudewijn R. Haverkort and Martin Leucker and Jaco van de Pol},
booktitle = {Formal Methods: Applications and Technology, 11th International Workshop, FMICS 2006 and 5th International Workshop PDMC 2006, Bonn, Germany, August 2627, and August 31, 2006, Revised Selected Papers},
publisher = {SpringerVerlag},
series = {Lecture Notes in Computer Science},
volume = {4346},
year = {2007},
isbn = {9783540709510},
pages = {301315},
ee = {http://dx.doi.org/10.1007/9783540709527_21},
} 
[inproceedings] bibtexM. Fränzle, "Verification of Hybrid Systems (Invited Tutorial)," in Proc. Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 37, 2007, Proceedings, 2007, p. 38.
@inproceedings{DBLP:conf/cav/Franzle07,
author = {Martin Fr{\"a}nzle},
title = {Verification of Hybrid Systems (Invited Tutorial)},
booktitle = {Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 37, 2007, Proceedings},
editor = {Werner Damm and Holger Hermanns},
year = {2007},
publisher = {SpringerVerlag},
series = {Lecture Notes in Computer Science},
volume = {4590},
pages = {38},
ee = {http://dx.doi.org/10.1007/9783540733683_7},
isbn = {9783540733676},
bibsource = {DBLP, http://dblp.unitrier.de} }
2006

[phdthesis] bibtexB. Badban, "Verification techniques for Extensions of equality logic," PhD Thesis , 2006.
@PhdThesis{badban07,
author = "Bahareh Badban", title = "Verification techniques for Extensions of equality logic", school = "Vrije Universiteit of Amsterdam", year = "2006", OPTmonth = "September", } 
[inproceedings] bibtexM. Fränzle, C. Herde, S. Ratschan, T. Schubert, und T. Teige, "Interval Constraint Solving Using Propositional SAT Solving Techniques," in Proc. Proceedings of the CP 2006 First International Workshop on the Integration of SAT and CP Techniques, 2006, pp. 8195.
@InProceedings{FraenzleEA:iSAT,
author = "Martin Fr{\"a}nzle and Christian Herde and Stefan Ratschan and Tobias Schubert and Tino Teige", title = "Interval Constraint Solving Using Propositional {SAT} Solving Techniques", booktitle = "Proceedings of the CP 2006 First International Workshop on the Integration of SAT and CP Techniques", pages = "8195", year = "2006", } 
[inproceedings] bibtexA. Metzner, M. Fränzle, C. Herde, und I. Stierand, "An Optimal Approach to the Task Allocation Problem on Hierarchical Architectures," in Proc. Proceedings of the 20th IEEE International Parallel and Distributed Processing Symposium, 2006.
@InProceedings{wpdrts,
author = "A. Metzner and M. Fr{\"a}nzle and C. Herde and I. Stierand", title = "{An Optimal Approach to the Task Allocation Problem on Hierarchical Architectures}", booktitle = "{Proceedings of the 20th IEEE International Parallel and Distributed Processing Symposium}", publisher = "IEEE Computer Society", year = "2006", access = "restricted", subproject = "R2,H2", bibtex = "wpdrts06.bib", annote = "(8 pages)", } 
[article] bibtexM. Fränzle und C. Herde, "HySAT: An Efficient Proof Engine for Bounded Model Checking of Hybrid Systems," Formal Methods in System Design, 2006.
@Article{FraenzleHerde05,
author = "Martin Fr{\"a}nzle and Christian Herde", title = "{HySAT}: An Efficient Proof Engine for Bounded Model Checking of Hybrid Systems", journal = "Formal Methods in System Design", year = "2006", publisher = "SpringerVerlag", keywords = "verification, bounded model checking, hybrid systems, infinitestate systems, decision procedures, satisfiability", subproject = "H2", language = "USenglish", access = "restricted", } 
[inproceedings] bibtexA. Metzner und C. Herde, "RTSAT  An Optimal and Efficient Approach to the Task Allocation Problem in Distributed Architectures," in Proc. Proceedings of the IEEE RealTime Systems Symposium, 2006, pp. 147156.
@InProceedings{rtss06,
author = "Alexander Metzner and Christian Herde", title = "{RTSAT}  An Optimal and Efficient Approach to the Task Allocation Problem in Distributed Architectures", booktitle = "Proceedings of the IEEE RealTime Systems Symposium", year = "2006", pages = "147156", publisher = "IEEE Computer Society", } 
[inproceedings] bibtexB. Badban, M. Fränzle, J. Peleska, und T. Teige, "Test Automation for Hybrid Systems," in Proc. Proceedings of the Third International Workshop on SOFTWARE QUALITY ASSURANCE (SOQUA 2006), Portland Oregon, USA, 2006, pp. 1421.
@InProceedings{bfpt2006a,
author = "Bahareh Badban and Martin Fr{\"{a}}nzle and Jan Peleska and Tino Teige", title = "Test Automation for Hybrid Systems", booktitle = "Proceedings of the Third International Workshop on SOFTWARE QUALITY ASSURANCE (SOQUA 2006)", pages = "1421", year = "2006", address = "Portland Oregon, USA", } 
[inproceedings] bibtexM. Swaminathan und M. Fränzle, "Robust ZoneBased Forward Reachability Analysis of Timed Automata," in Proc. Proceedings of the 7th School on Modelling and Verifying of parallel Processes (MOVEP 06), Bordeaux, France, 2006.
@InProceedings{SwaFr06,
author = "Mani Swaminathan and Martin Fr{\"a}nzle", title = "Robust ZoneBased Forward Reachability Analysis of Timed Automata", booktitle = "Proceedings of the 7th School on Modelling and Verifying of parallel Processes (MOVEP 06)", year = "2006", month = jun, address = "Bordeaux, France", }
2005

[inproceedings] bibtexA. Metzner, M. Fränzle, C. Herde, und I. Stierand, "Scheduling Distributed RealTime Systems by Satisfiability Checking," in Proc. Proceedings of the IEEE Conference on Embedded and RealTime Computing Systems and Applications, 2005, pp. 409415.
@InProceedings{rtcsa,
author = "A. Metzner and M. Fr{\"a}nzle and C. Herde and I. Stierand", title = "{Scheduling Distributed RealTime Systems by Satisfiability Checking}", booktitle = "Proceedings of the IEEE Conference on Embedded and RealTime Computing Systems and Applications", publisher = "IEEE Computer Society", pages = "409415", year = "2005", subproject = "R2,H2", access = "restricted", } 
[inproceedings] bibtexM. Fränzle und M. R. Hansen, "A robust interpretation of duration calculus," in Proc. Proceedings of ICTAC 05 International Colloquium on Theoretical Aspects of Computing, 2005, pp. 257271.
@InProceedings{Franzle05,
author = "M. Fr{\"a}nzle and M. R. Hansen", title = "A robust interpretation of duration calculus", booktitle = "Proceedings of ICTAC 05 International Colloquium on Theoretical Aspects of Computing", year = "2005", editor = "Dang Van Hung and Martin Wirsing", volume = "3722", series = Lecture Notes in Computer Science, pages = "257271", publisher = "SpringerVerlag Verlag", } 
[article] bibtexM. Fränzle und C. Herde, "Efficient proof engines for bounded model checking of hybrid systems," Electronic Notes in Theoretical Computer Science, vol. 133, pp. 119137, 2005.
@Article{Franzle05b,
author = "M. Fr{\"a}nzle and C. Herde", title = "Efficient proof engines for bounded model checking of hybrid systems", journal = "Electronic Notes in Theoretical Computer Science", year = "2005", volume = "133", number = "", pages = "119137", month = "", note = "", } 
[inproceedings] bibtexA. Metzner und C. Herde, "RTSAT  Scheduling Tasks in Distributed RealTime Systems by Enhanced Satisifiability Checking," in Proc. Proceedings of the IEEE RealTime Systems Symposium, Work in Progress Session, 2005.
@InProceedings{rtss05,
author = "Alexander Metzner and Christian Herde", title = "{{RTSAT}  Scheduling Tasks in Distributed RealTime Systems by Enhanced Satisifiability Checking}", booktitle = "Proceedings of the IEEE RealTime Systems Symposium, Work in Progress Session", year = "2005", } 
[inproceedings] bibtexJ. Enslev, A. Nielsen, M. Fränzle, und M. R. Hansen, "Bounded Model Construction for Duration Calculus," in Proc. Proceedings of the 17th Nordic Workshop on Programming Theory (NWPT 05), Københavns Universitet, 2005.
@InProceedings{EnslevNielsenFraenzleHansenBMCforDC,
author = "Jacob Enslev and AnneSofie Nielsen and Martin Fr{\"a}nzle and Michael R. Hansen", title = "Bounded Model Construction for Duration Calculus", booktitle = "Proceedings of the 17th Nordic Workshop on Programming Theory (NWPT 05)", editor = "Jones, Neil et al.", year = "2005", month = oct, address = "K{\o}benhavns Universitet", } 
[inproceedings] bibtexM. Swaminathan und M. Fränzle, "Automatic and scalable verification of robust realtime systems," in Proc. Proceedings of the 17th Nordic Workshop on Programming Theory (NWPT 05), Københavns Universitet, 2005.
@InProceedings{SwaminathanFraenzle,
author = "Mani Swaminathan and Martin Fr{\"a}nzle", title = "Automatic and scalable verification of robust realtime systems", booktitle = "Proceedings of the 17th Nordic Workshop on Programming Theory (NWPT 05)", editor = "Jones, Neil et al.", year = "2005", month = oct, address = "K{\o}benhavns Universitet", }
2004

[inproceedings] bibtexM. Fränzle und M. R. Hansen, "A robust interpretation of duration calculus," in Proc. Proceedings of NWPT 04 16th Nordic Workshop on Programming Theory, 2004.
@InProceedings{Franzle04,
author = "M. Fr{\"a}nzle and M. R. Hansen", title = "A robust interpretation of duration calculus", booktitle = "Proceedings of NWPT 04 16th Nordic Workshop on Programming Theory", year = "2004", editor = "P. Pettersson and W. Yi", pages = "", organization = "Uppsala University", publisher = "Dept. of Information Technology", address = "", month = "", note = "", } 
[article] bibtexM. Fränzle, "Modelchecking densetime duration calculus," Formal Aspects of Computing, vol. 16, iss. 2, pp. 121139, 2004.
@Article{Franzle04a,
author = "M. Fr{\"a}nzle", title = "Modelchecking densetime duration calculus", journal = "Formal Aspects of Computing", year = "2004", volume = "16", number = "2", pages = "121139", month = "", note = "", publisher = "SpringerVerlag Verlag", } 
[inproceedings] bibtexB. Becker, M. Behle, F. Eisenbrand, M. Fränzle, M. Herbstritt, C. Herde, J. Hoffmann, D. Kröning, B. Nebel, I. Polian, und R. Wimmer, "Bounded model checking and inductive verification of hybrid discretecontinuous systems," in Proc. GI/ITG/GMM Workshop 'Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen', 2004, pp. 6575.
@InProceedings{Franzle04b,
author = "B. Becker and M. Behle and F. Eisenbrand and M. Fr{\"a}nzle and M. Herbstritt and C. Herde and J. Hoffmann and D. Kr{\"o}ning and B. Nebel and I. Polian and R. Wimmer", title = "Bounded model checking and inductive verification of hybrid discretecontinuous systems", booktitle = "{GI/ITG/GMM Workshop 'Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen'}", year = "2004", editor = "", pages = "6575", organization = "", publisher = "Universit{\"a}t Kaiserslautern", address = "", month = feb, note = "", }
2003

[inproceedings] bibtexM. Fränzle und C. Herde, "Efficient SAT Engines for Concise Logics: Accelerating Proof Search for ZeroOne Linear Constraint Systems," in Proc. Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings of the 10th International Conference, LPAR 2003, Almaty, Kazakhstan, September 2226, 2003, 2003, pp. 302316.
@inproceedings{FraenzleHerdeLPAR2003,
author = {Martin Fr{\"a}nzle and Christian Herde},
title = {Efficient SAT Engines for Concise Logics: Accelerating Proof Search for ZeroOne Linear Constraint Systems},
editor = {Mosche Vardi and Andrei Voronkov},
year = 2003, isbn = {9783540201014},
publisher = {Springer},
booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings of the 10th International Conference, LPAR 2003, Almaty, Kazakhstan, September 2226, 2003},
series = {Lecture Notes in Artificial Intelligence},
volume = 2850, pages = {302316} } 
[article] bibtex  Dokument aufrufenM. Fränzle, J. Niehaus, A. Metzner, und W. Damm, "A Semantics for Distributed Execution of Statemate," Formal Aspects of Computing, vol. V15, iss. 4, pp. 390405, 2003.
@article{franzle_03_semantics,
author = {Fr\"{a}nzle, Martin and Niehaus, J\"{u}rgen and Metzner, Alexander and Damm, Werner },
citeulikearticleid = {887517},
doi = {http://dx.doi.org/10.1007/s0016500300154},
journal = {Formal Aspects of Computing},
keywords = {2003, distributed, semantics, statecharts, statemate},
month = {December},
number = {4},
pages = {390405},
postedat = {20061006 20:32:37},
priority = {3},
title = {A Semantics for Distributed Execution of Statemate},
url = {http://dx.doi.org/10.1007/s0016500300154},
volume = {V15},
year = {2003} }
2002

[inproceedings] bibtexM. Fränzle, "Take It NPEasy: Bounded Model Construction for Duration Calculus," in Proc. FTRTFT '02: Proceedings of the 7th International Symposium on Formal Techniques in RealTime and FaultTolerant Systems, London, UK, 2002, pp. 245264.
@inproceedings{707111,
author = {Martin Fr\"{a}nzle},
title = {Take It NPEasy: Bounded Model Construction for Duration Calculus},
booktitle = {FTRTFT '02: Proceedings of the 7th International Symposium on Formal Techniques in RealTime and FaultTolerant Systems},
year = {2002},
series= {Lecture Notes in Computer Science},
volume= {2469},
isbn = {3540441654},
pages = {245264},
publisher = {SpringerVerlag},
address = {London, UK},
}