-
-
Grochowski, M., Simon, H., Bohlender, D., Kowalewski, S., Löcklin, A., Müller, T., Jazdi, N., Zeller, A., and Weyrich, M., "Formale Methoden für rekonfigurierbare cyber-physische Systeme in der Produktion", Automatisierungstechnik, vol. 68, iss. 1, pp. 3-14, 2020
Formale Methoden f{\"u}r rekonfigurierbare cyber-physische Systeme in der Produktion
Bibtex entry :
@article { GSB+20,
author = { Grochowski, Marco and Simon, Hendrik and Bohlender, Dimitri
and Kowalewski, Stefan and L{\"o}cklin, Andreas and
M{\"u}ller, Timo and Jazdi, Nasser and Zeller, Andreas and
Weyrich, Michael },
title = { Formale Methoden f{\"u}r rekonfigurierbare cyber-physische
Systeme in der Produktion },
journal = { Automatisierungstechnik },
publisher = { De Gruyter },
pages = { 3-14 },
volume = { 68 },
number = { 1 },
year = { 2020 },
address = { Berlin },
issn = { 2196-677X },
doi = { 10.1515/auto-2019-0115 },
typ = { PUB:(DE-HGF)16 },
reportid = { RWTH-2019-12214 },
cin = { 122810 / 120000 },
url = { https://www.degruyter.com/view/j/auto.2020.68.issue-1/auto-2019-0115/auto-2019-0115.xml },
}
-
-
Bohlender, D. and Kowalewski, S., "Leveraging Horn clause solving for compositional verification of PLC software", Discrete event dynamic systems, vol. 30, pp. 1-24, 2019
Leveraging Horn clause solving for compositional verification of PLC software
Bibtex entry :
@article { BK19,
author = { Bohlender, Dimitri and Kowalewski, Stefan },
title = { Leveraging Horn clause solving for compositional
verification of PLC software },
journal = { Discrete event dynamic systems },
publisher = { Springer Science + Business Media B.V },
pages = { 1-24 },
volume = { 30 },
year = { 2019 },
address = { Dordrecht [u.a.] },
issn = { 0924-6703 },
doi = { 10.1007/s10626-019-00296-8 },
typ = { PUB:(DE-HGF)16 },
reportid = { RWTH-2019-12207 },
cin = { 122810 / 120000 },
}
-
-
Bohlender, D. and Kowalewski, S., "Design and Verification of Restart-robust Industrial Control Software", in Proc. Integrated Formal Methods - 14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018, 2018, Springer, pp. 47-68.
Design and Verification of Restart-robust Industrial Control Software
Bibtex entry :
@inproceedings { BK18a,
author = { Bohlender, Dimitri and Kowalewski, Stefan },
title = { Design and Verification of Restart-robust Industrial Control
Software },
booktitle = { Integrated Formal Methods - 14th International Conference,
IFM 2018, Maynooth, Ireland, September 5-7, 2018 },
publisher = { Springer },
publishedas = { Druck Online },
isbn = { 978-3-319-98938-9 },
language = { eng },
pages = { 47--68 },
year = { 2018 },
timestamp = { 2018.06.18 },
i11key = { conference },
i11projectkey = { Arcade },
for_reporting_period = { 2018 },
}
-
-
Simon, H., Triefenbach, L., and Kowalewski, S., "Structural Concolic Testing fpr Sequential Function Chart", in Proc. 14th International Workshop on Discrete Event Systems, WODES 2018, Sorrento Coast, Italy, May 30 - June 1, 2018, 2018, vol. 51, Elsevier, pp. 422-427.
Structural Concolic Testing fpr Sequential Function Chart
Bibtex entry :
@inproceedings { STK18,
author = { Simon, Hendrik and Triefenbach, Lucas and Kowalewski, Stefan },
editor = { Gianmaria De Tommasi },
title = { Structural Concolic Testing fpr Sequential Function Chart },
booktitle = { 14th International Workshop on Discrete Event Systems, WODES
2018, Sorrento Coast, Italy, May 30 - June 1, 2018 },
volume = { 51 },
publisher = { Elsevier },
publishedas = { Online },
issn = { 2405-8963 },
language = { eng },
pages = { 422--427 },
year = { 2018 },
timestamp = { 2018.06.06 },
i11key = { conference },
i11projectkey = { Arcade },
url = { https://www.sciencedirect.com/journal/ifac-papersonline/vol/51/issue/7 },
for_reporting_period = { 2018 },
}
-
-
Bohlender, D. and Kowalewski, S., "Compositional Verification of PLC Software using Horn Clauses and Mode Abstraction", in Proc. 14th International Workshop on Discrete Event Systems, WODES 2018, Sorrento Coast, Italy, May 30 - June 1, 2018, 2018, IFAC, pp. 428-433.
Compositional Verification of PLC Software using Horn Clauses and Mode Abstraction
Bibtex entry :
@inproceedings { BK18,
author = { Bohlender, Dimitri and Kowalewski, Stefan },
title = { Compositional Verification of PLC Software using Horn
Clauses and Mode Abstraction },
booktitle = { 14th International Workshop on Discrete Event Systems, WODES
2018, Sorrento Coast, Italy, May 30 - June 1, 2018 },
publisher = { IFAC },
publishedas = { Online },
issn = { 2405-8963 },
language = { eng },
pages = { 428--433 },
year = { 2018 },
timestamp = { 2018.03.05 },
i11key = { conference },
i11projectkey = { Arcade },
for_reporting_period = { 2018 },
}
-
-
Bohlender, D., Hamm, D., and Kowalewski, S., "Cycle-Bounded Model Checking of PLC Software via Dynamic Large-Block Encoding", in Proc. Proceedings of the 33rd Annual ACM Symposium on Applied Computing, SAC 2018, Pau, France, April 09-13, 2018, 2018, ACM, pp. 1891-1898.
Cycle-Bounded Model Checking of PLC Software via Dynamic Large-Block Encoding
Bibtex entry :
@inproceedings { BHK18,
author = { Bohlender, Dimitri and Hamm, Daniel and Kowalewski, Stefan },
title = { Cycle-Bounded Model Checking of PLC Software via Dynamic
Large-Block Encoding },
booktitle = { Proceedings of the 33rd Annual ACM Symposium on Applied
Computing, SAC 2018, Pau, France, April 09-13, 2018 },
publisher = { ACM },
publishedas = { Druck Online },
isbn = { 978-1-4503-5191-1 },
language = { eng },
pages = { 1891--1898 },
year = { 2018 },
timestamp = { 2018.01.10 },
i11key = { conference },
i11projectkey = { Arcade },
for_reporting_period = { 2018 },
}
-
-
Obster, M. and Kowalewski, S., "A Live Static Code Analysis Architecture for PLC Software", in Proc. Proceedings of IEEE International Conference on Emerging Technology & Factory Automation, 2017, IEEE, pp. 263-266.
A Live Static Code Analysis Architecture for PLC Software
Bibtex entry :
@inproceedings { OK17,
author = { Obster, Mathias and Kowalewski, Stefan },
title = { A Live Static Code Analysis Architecture for PLC Software },
booktitle = { Proceedings of IEEE International Conference on Emerging
Technology & Factory Automation },
publisher = { IEEE },
publishedas = { Online },
isbn = { 978-1-5090-6505-9 },
issn = { 1946-0759 },
language = { eng },
pages = { 263--266 },
year = { 2017 },
timestamp = { 2017.11.23 },
i11key = { conference },
i11projectkey = { Arcade },
url = { https://publications.embedded.rwth-aachen.de/file/7a },
for_reporting_period = { 2017 },
}
-
-
Ulewicz, S., Vogel-Heuser, B., Simon, H., Bohlender, D., Obster, M., and Kowalewski, S., "A Priori Test Coverage Estimation for Automated Production Systems", in Proc. 2017 22nd IEEE International Conference on Emerging Technologies and Factory Automation (ETFA), 2017, IEEE, pp. 1-4.
A Priori Test Coverage Estimation for Automated Production Systems
Bibtex entry :
@inproceedings { UVS+17,
author = { Ulewicz, Sebastian and Vogel-Heuser, Birgit and Simon,
Hendrik and Bohlender, Dimitri and Obster, Mathias and
Kowalewski, Stefan },
title = { A Priori Test Coverage Estimation for Automated Production
Systems },
booktitle = { 2017 22nd IEEE International Conference on Emerging
Technologies and Factory Automation (ETFA) },
publisher = { IEEE },
publishedas = { Druck Online },
isbn = { 978-1-5090-6505-9 },
issn = { 1946-0759 },
language = { eng },
pages = { 1--4 },
year = { 2017 },
timestamp = { 2017.10.27 },
i11key = { conference },
i11projectkey = { Arcade },
url = { http://ieeexplore.ieee.org/document/8247704/ },
for_reporting_period = { 2017 },
}
-
-
Bohlender, D., Simon, H., Kowalewski, S., and Hauck-Stattelmann, S., "Symbolische Ausführung zum Testen von SPS-Programmen", in Proc. Automation 2016, 07.06.2016-08.06.2016, Baden-Baden, Germany, 2016, VDI Verlag GmbH, pp. 77-88.
Symbolische Ausf{\"u}hrung zum Testen von SPS-Programmen
Bibtex entry :
@inproceedings { BSKH16,
author = { Bohlender, Dimitri and Simon, Hendrik and Kowalewski, Stefan
and Hauck-Stattelmann, Stefan },
title = { Symbolische Ausf{\"u}hrung zum Testen von SPS-Programmen },
booktitle = { Automation 2016, 07.06.2016-08.06.2016, Baden-Baden, Germany },
publisher = { VDI Verlag GmbH },
publishedas = { Druck },
isbn = { 978-3-18-092284-0 },
language = { ger },
pages = { 77--88 },
year = { 2016 },
timestamp = { 2016.08.03 },
i11key = { conference },
i11projectkey = { Arcade },
for_reporting_period = { 2016 },
}
-
-
Bohlender, D., Simon, H., Friedrich, N., Kowalewski, S., and Hauck-Stattelmann, S., "Concolic Test Generation for PLC Programs using Coverage Metrics", in Proc. 13th International Workshop on Discrete Event Systems, WODES 2016, Xi'an, China, May 30 - June 1, 2016, 2016, IEEE, pp. 432-437.
Concolic Test Generation for PLC Programs using Coverage Metrics
Bibtex entry :
@inproceedings { BSF+16,
author = { Bohlender, Dimitri and Simon, Hendrik and Friedrich, Nico
and Kowalewski, Stefan and Hauck-Stattelmann, Stefan },
title = { Concolic Test Generation for PLC Programs using Coverage
Metrics },
booktitle = { 13th International Workshop on Discrete Event Systems, WODES
2016, Xi'an, China, May 30 - June 1, 2016 },
publisher = { IEEE },
publishedas = { Druck },
isbn = { 978-1-5090-4190-9 },
language = { eng },
pages = { 432--437 },
year = { 2016 },
timestamp = { 2016.06.27 },
i11key = { conference },
i11projectkey = { Arcade },
for_reporting_period = { 2016 },
}
-
-
Bohlender, D., Simon, H., and Kowalewski, S., "Symbolic Verification of PLC Safety-Applications based on PLCopen Automata", in Proc. 19th GI/ITG/GMM Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, MBMV 2016, Freiburg im Breisgau, Germany, March 1-2, 2016., 2016, Albert-Ludwigs-Universität Freiburg, pp. 33-45.
Symbolic Verification of PLC Safety-Applications based on PLCopen Automata
Bibtex entry :
@inproceedings { BSK16,
author = { Bohlender, Dimitri and Simon, Hendrik and Kowalewski, Stefan },
editor = { Ralf Wimmer },
title = { Symbolic Verification of PLC Safety-Applications based on
PLCopen Automata },
booktitle = { 19th GI/ITG/GMM Workshop Methoden und Beschreibungssprachen
zur Modellierung und Verifikation von Schaltungen und
Systemen, MBMV 2016, Freiburg im Breisgau, Germany, March
1-2, 2016. },
publisher = { Albert-Ludwigs-Universit{\"{a}}t Freiburg },
publishedas = { Online },
isbn = { 978-3-00-052380-9 },
language = { eng },
pages = { 33--45 },
year = { 2016 },
timestamp = { 2016.03.03 },
i11key = { conference },
i11projectkey = { Arcade },
for_reporting_period = { 2016 },
}
-
-
Biallas, S., Friedrich, N., Simon, H., and Kowalewski, S., "Automatic Error Cause Localization of Faulty PLC Programs", IFAC-PapersOnLine, vol. 48, pp. 79-84, 2015
Automatic Error Cause Localization of Faulty PLC Programs
Bibtex entry :
@article { BFSK15,
author = { Biallas, Sebastian and Friedrich, Nico and Simon, Hendrik
and Kowalewski, Stefan },
title = { Automatic Error Cause Localization of Faulty PLC Programs },
journal = { IFAC-PapersOnLine },
year = { 2015 },
volume = { 48 },
pages = { 79--84 },
publisher = { Elsevier Ltd },
publishedas = { Online Druck },
issn = { 1474-6670 },
i11key = { conference },
i11projectkey = { Arcade },
language = { eng },
url = { http://www.sciencedirect.com/science/article/pii/S2405896315007156 },
timestamp = { 2015.09.21 },
for_reporting_period = { 2015 },
}
-
-
Biallas, S., Simon, H., Kowalewski, S., Hauck-Stattelmann, S., and Schlich, B., "Automatische Testfallgenerierung für SPS-Programme mittels Zeilenüberdeckung", in Proc. AUTOMATION 2015, 2015, VDI, pp. 100-111.
Automatische Testfallgenerierung f{\"u}r SPS-Programme mittels Zeilen{\"u}berdeckung
Bibtex entry :
@inproceedings { BSK+15,
author = { Biallas, Sebastian and Simon, Hendrik and Kowalewski, Stefan
and Hauck-Stattelmann, Stefan and Schlich, Bastian },
title = { Automatische Testfallgenerierung f{\"u}r SPS-Programme
mittels Zeilen{\"u}berdeckung },
booktitle = { AUTOMATION 2015 },
publisher = { VDI },
publishedas = { Druck },
language = { ger },
pages = { 100--111 },
year = { 2015 },
timestamp = { 2015.07.08 },
i11key = { conference },
i11projectkey = { Arcade },
url = { {http://publications.embedded.rwth-aachen.de/file/5r} },
for_reporting_period = { 2015 },
}
-
-
Hauck-Stattelmann, S., Biallas, S., Schlich, B., Kowalewski, S., and Jetley, R., "Analyzing the Restart Behavior of Industrial Control Applications", in Proc. FM 2015: Formal Methods, 2015, vol. 9109 in Lecture Notes in Computer Science, Springer International Publishing, pp. 585-588.
Analyzing the Restart Behavior of Industrial Control Applications
Bibtex entry :
@inproceedings { HBS+15,
keywords = { Static Analysis; Abstract Interpretation; Programmable Logic
Controllers },
author = { Hauck-Stattelmann, Stefan and Biallas, Sebastian and
Schlich, Bastian and Kowalewski, Stefan and Jetley, Raoul },
editor = { Bj{\o}rner, Nikolaj and de Boer, Frank },
title = { Analyzing the Restart Behavior of Industrial Control
Applications },
booktitle = { FM 2015: Formal Methods },
series = { Lecture Notes in Computer Science },
volume = { 9109 },
publisher = { Springer International Publishing },
publishedas = { Druck Online },
isbn = { 978-3-319-19248-2 },
language = { eng },
pages = { 585--588 },
year = { 2015 },
timestamp = { 2015.06.03 },
i11key = { conference },
i11projectkey = { Arcade },
url = { http://publications.embedded.rwth-aachen.de/file/5u },
for_reporting_period = { 2015 },
}
-
-
Gückel, D., "Synthesis of State Space Generators for Model Checking Microcontroller Code," PhD Thesis , RWTH Aachen, 2014.
{S}ynthesis of {S}tate {S}pace {G}enerators for {M}odel {C}hecking {M}icrocontroller {C}ode
Bibtex entry :
@phdthesis { Gue14,
institution = { RWTH Aachen },
keywords = { formal verification, model checking, hardware description,
retargeting, embedded software },
number = { AIB-2014-15 },
timestamp = { 2015.06.01 },
author = { G{\"u}ckel, Dominique },
title = { {S}ynthesis of {S}tate {S}pace {G}enerators for {M}odel
{C}hecking {M}icrocontroller {C}ode },
school = { Fakult{\"a}t f{\"u}r Mathematik, Informatik und
Naturwissenschaften der RWTH Aachen },
type = { Dissertation },
year = { 2014 },
month = { November },
i11key = { thesis },
i11projectkey = { Arcade },
url = { http://aib.informatik.rwth-aachen.de/2014/2014-15.pdf },
for_reporting_period = { 2014 },
}
-
-
Stattelmann, S., Biallas, S., Schlich, B., and Kowalewski, S., "Applying Static Code Analysis on Industrial Controller Code", in Proc. 19th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA), 2014, IEEE, Work in Progress Best Paper Award.
Applying Static Code Analysis on Industrial Controller Code
Bibtex entry :
@inproceedings { SBSK14,
author = { Stattelmann, Stefan and Biallas, Sebastian and Schlich,
Bastian and Kowalewski, Stefan },
title = { Applying Static Code Analysis on Industrial Controller Code },
booktitle = { 19th IEEE International Conference on Emerging Technologies
and Factory Automation (ETFA) },
publisher = { IEEE },
publishedas = { Druck Online },
isbn = { 978-1-4799-4845-1 },
language = { eng },
year = { 2014 },
timestamp = { 2014.09.17 },
i11key = { conference },
i11projectkey = { Arcade },
note = { Work in Progress Best Paper Award },
for_reporting_period = { 2014 },
}
-
-
Biallas, S., Kowalewski, S., Stattelmann, S., and Schlich, B., "Efficient Handling of States in Abstract Interpretation of Industrial Programmable Logic Controller Code", in Proc. Proceedings of the 12th International Workshop on Discrete Event Systems, Cachan, France, 2014, IFAC, pp. 400-405.
Efficient Handling of States in Abstract Interpretation of Industrial Programmable Logic Controller Code
Bibtex entry :
@inproceedings { BKSS14,
address = { Cachan, France },
author = { Biallas, Sebastian and Kowalewski, Stefan and Stattelmann,
Stefan and Schlich, Bastian },
title = { Efficient Handling of States in Abstract Interpretation of
Industrial Programmable Logic Controller Code },
booktitle = { Proceedings of the 12th International Workshop on Discrete
Event Systems },
publisher = { IFAC },
publishedas = { Druck Online },
language = { eng },
pages = { 400--405 },
year = { 2014 },
timestamp = { 2014.02.24 },
i11key = { conference },
i11projectkey = { Arcade },
for_reporting_period = { 2014 },
}
-
-
Brauer, J., "Automatic Abstraction for Bit-Vectors using Decision Procedures," PhD Thesis , 2013.
{A}utomatic {A}bstraction for {B}it-{V}ectors using {D}ecision {P}rocedures
Bibtex entry :
@phdthesis { Bra13,
author = { Brauer, J{\"o}rg },
title = { {A}utomatic {A}bstraction for {B}it-{V}ectors using
{D}ecision {P}rocedures },
school = { Fakult{\"a}t f{\"u}r Mathematik, Informatik und
Naturwissenschaften der RWTH Aachen },
type = { Dissertation },
year = { 2013 },
month = { November },
issn = { 0935–3232 },
i11key = { thesis },
url = { http://publications.embedded.rwth-aachen.de/file/4y },
keywords = { abstract interpretation, automatic abstraction, sat solving,
decision procedures },
i11projectkey = { Arcade },
note = { AIB-2013-14 },
timestamp = { 2014.02.03 },
for_reporting_period = { 2013 },
}
-
-
Brauer, J., King, A., and Kowalewski, S., "Abstract interpretation of microcontroller code: Intervals meet congruences", Science of Computer Programming. Methods of Software Design: Techniques and Applications, vol. 78, issue 7, pp. 862-883, 2013
Abstract interpretation of microcontroller code: Intervals meet congruences
Bibtex entry :
@article { BKK13,
author = { Brauer, J{\"o}rg and King, Andy and Kowalewski, Stefan },
title = { Abstract interpretation of microcontroller code: Intervals
meet congruences },
journal = { Science of Computer Programming. Methods of Software Design:
Techniques and Applications },
year = { 2013 },
volume = { 78, issue 7 },
pages = { 862--883 },
publisher = { Elsevier },
publishedas = { Druck },
issn = { 0167-6423 },
i11key = { journal },
language = { eng },
timestamp = { 2013.07.08 },
i11projectkey = { Arcade },
for_reporting_period = { 2013 },
}
-
-
Biallas, S., Giacobbe, M., and Kowalewski, S., "Predicate Abstraction for Programmable Logic Controllers", in Proc. 18th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2013), 2013, vol. 8187 in Lecture Notes in Computer Science, Springer Berlin Heidelberg, pp. 123-138.
Predicate Abstraction for Programmable Logic Controllers
Bibtex entry :
@inproceedings { BGK13,
author = { Biallas, Sebastian and Giacobbe, Mirco and Kowalewski,
Stefan },
editor = { Pecheur, Charles and Dierkes, Michael },
title = { Predicate Abstraction for Programmable Logic Controllers },
booktitle = { 18th International Workshop on Formal Methods for Industrial
Critical Systems (FMICS 2013) },
series = { Lecture Notes in Computer Science },
number = { 8187 },
publisher = { Springer Berlin Heidelberg },
publishedas = { Druck },
isbn = { 978-3-642-41009-3 },
language = { eng },
pages = { 123--138 },
year = { 2013 },
timestamp = { 2013.06.27 },
i11key = { conference },
i11projectkey = { Arcade },
volume = { 8187 },
url = { http://publications.embedded.rwth-aachen.de/file/4u },
for_reporting_period = { 2013 },
}
-
-
Biallas, S., Bohlender, D., and Kowalewski, S., "Boolean and Modular Abstractions for Programmable Logic Controllers", in Proc. Dependable Control of Discrete Systems (DCDS'13), 2013, IEEE, pp. 97-102.
Boolean and Modular Abstractions for Programmable Logic Controllers
Bibtex entry :
@inproceedings { BBK13,
author = { Biallas, Sebastian and Bohlender, Dimitri and Kowalewski,
Stefan },
title = { Boolean and Modular Abstractions for Programmable Logic
Controllers },
booktitle = { Dependable Control of Discrete Systems (DCDS'13) },
publisher = { IEEE },
publishedas = { Druck },
isbn = { 978-3-902823-49-6 },
issn = { 1474-6670 },
language = { eng },
pages = { 97--102 },
year = { 2013 },
timestamp = { 2013.06.06 },
i11key = { conference },
i11projectkey = { Arcade },
for_reporting_period = { 2013 },
}
-
-
Biallas, S., Kamin, V., Kowalewski, S., Schlich, B., Sehestedt, S., and Stattelmann, S., "Verifikation von sicherheitsgerichteten SPS-Programmen mit Hilfe von Safety-Automaten", in Proc. Automation 2013, 2013 in VDI Berichte, VDI-Verlag, pp. 75-79, Langfassung auf CD-ROM.
Verifikation von sicherheitsgerichteten SPS-Programmen mit Hilfe von Safety-Automaten
Bibtex entry :
@inproceedings { BKK+13,
author = { Biallas, Sebastian and Kamin, Volker and Kowalewski, Stefan
and Schlich, Bastian and Sehestedt, Stephan and Stattelmann,
Stefan },
editor = { VDI Wissensforum },
title = { Verifikation von sicherheitsgerichteten SPS-Programmen mit
Hilfe von Safety-Automaten },
booktitle = { Automation 2013 },
series = { VDI Berichte },
publisher = { VDI-Verlag },
publishedas = { Druck },
isbn = { 978-3-18-092209-6 },
language = { ger },
pages = { 75--79 },
year = { 2013 },
timestamp = { 2013.04.16 },
i11key = { conference },
i11projectkey = { Arcade },
note = { Langfassung auf CD-ROM },
for_reporting_period = { 2013 },
}
-
-
Biallas, S., Brauer, J., and Kowalewski, S., "Arcade.PLC: A Verification Platform for Programmable Logic Controllers", in Proc. Proceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering, 2012 in ASE 2012, ACM, pp. 338-341.
{Arcade.PLC}: A Verification Platform for Programmable Logic Controllers
Bibtex entry :
@inproceedings { BBK12b,
author = { Biallas, Sebastian and Brauer, J{\"o}rg and Kowalewski,
Stefan },
title = { {Arcade.PLC}: A Verification Platform for Programmable Logic
Controllers },
booktitle = { Proceedings of the 27th IEEE/ACM International Conference on
Automated Software Engineering },
series = { ASE 2012 },
publisher = { ACM },
publishedas = { Druck Online },
isbn = { 978-1-4503-1204-2 },
language = { eng },
pages = { 338--341 },
year = { 2012 },
timestamp = { 2012.09.16 },
i11key = { conference },
i11projectkey = { Arcade },
url = { http://publications.embedded.rwth-aachen.de/file/3w },
for_reporting_period = { 2012 },
}
-
-
Biallas, S., Kowalewski, S., and Schlich, B., "Automatische Wertebereichsanalyse -- Formale Verifikation für SPS-Programme", Automatisierungstechnische Praxis (atp EDITION), 54. Jahrgang, 7-8/2012, pp. 68-75, 2012
Automatische Wertebereichsanalyse -- Formale Verifikation f{\"u}r SPS-Programme
Bibtex entry :
@article { BKS12c,
author = { Biallas, Sebastian and Kowalewski, Stefan and Schlich,
Bastian },
title = { Automatische Wertebereichsanalyse -- Formale Verifikation
f{\"u}r SPS-Programme },
journal = { Automatisierungstechnische Praxis (atp EDITION), 54.
Jahrgang, 7-8/2012 },
year = { 2012 },
pages = { 68--75 },
publisher = { Oldenbourg Industrieverlag },
publishedas = { Druck },
issn = { 2190-4111 },
i11key = { journal },
i11projectkey = { Arcade },
language = { ger },
timestamp = { 2012.08.02 },
for_reporting_period = { 2012 },
}
-
-
Biallas, S., Kowalewski, S., and Schlich, B., "Range and Value-Set Analysis for Programmable Logic Controllers", in Proc. Proceedings of the 11th International Workshop on Discrete Event Systems, Guadalajara, Mexico, 2012, IFAC, pp. 378-383.
Range and Value-Set Analysis for Programmable Logic Controllers
Bibtex entry :
@inproceedings { BKS12b,
address = { Guadalajara, Mexico },
author = { Biallas, Sebastian and Kowalewski, Stefan and Schlich,
Bastian },
title = { Range and Value-Set Analysis for Programmable Logic
Controllers },
booktitle = { Proceedings of the 11th International Workshop on Discrete
Event Systems },
publisher = { IFAC },
publishedas = { Druck Online },
isbn = { 978-3-902823-28-1 },
language = { eng },
pages = { 378--383 },
year = { 2012 },
timestamp = { 2012.06.26 },
i11key = { conference },
i11projectkey = { Arcade },
url = { http://publications.embedded.rwth-aachen.de/file/3x },
for_reporting_period = { 2012 },
}
-
-
Biallas, S., Brauer, J., King, A., and Kowalewski, S., "Loop Leaping with Closures", in Proc. 19th Static Analysis Symposium, 2012 in Lecture Notes in Computer Science, Springer Berlin Heidelberg, pp. 214-230.
Loop Leaping with Closures
Bibtex entry :
@inproceedings { BBKK12,
author = { Biallas, Sebastian and Brauer, J{\"o}rg and King, Andy and
Kowalewski, Stefan },
editor = { Min{\'e}, Antoine and Schmidt, David },
title = { Loop Leaping with Closures },
booktitle = { 19th Static Analysis Symposium },
series = { Lecture Notes in Computer Science },
publisher = { Springer Berlin Heidelberg },
publishedas = { Druck Online },
isbn = { 978-3-642-33124-4 },
language = { eng },
pages = { 214--230 },
year = { 2012 },
timestamp = { 2012.05.22 },
i11key = { conference },
i11projectkey = { Arcade },
for_reporting_period = { 2012 },
}
-
-
Biallas, S., Kowalewski, S., and Schlich, B., "Automatische Wertebereichsanalyse von SPS-Programmen", in Proc. AUTOMATION 2012, Baden-Baden, Germany, Düsseldorf, 2012 in VDI-Berichte, VDI-Verlag, pp. 79-83, Long version (12 pages) on CD-ROM.
Automatische Wertebereichsanalyse von SPS-Programmen
Bibtex entry :
@inproceedings { BKS12a,
address = { D{\"u}sseldorf },
author = { Biallas, Sebastian and Kowalewski, Stefan and Schlich,
Bastian },
title = { Automatische Wertebereichsanalyse von SPS-Programmen },
booktitle = { AUTOMATION 2012, Baden-Baden, Germany },
publisher = { VDI-Verlag },
publishedas = { Druck },
series = { VDI-Berichte },
number = { 2171 },
isbn = { 978-3-18-092171-6 },
language = { ger },
pages = { 79--83 },
year = { 2012 },
timestamp = { 2012.04.20 },
i11key = { conference },
i11projectkey = { Arcade },
for_reporting_period = { 2012 },
note = { Long version (12 pages) on CD-ROM },
}
-
-
Brauer, J. and Simon, A., "Inferring Definite Counterexamples Through Under-Approximation", in Proc. NASA Formal Methods, 2012, vol. 7226 in Lecture Notes in Computer Science, Springer, pp. 54-69.
Inferring Definite Counterexamples Through Under-Approximation
Bibtex entry :
@inproceedings { BS12,
author = { Brauer, J{\"o}rg and Simon, Axel },
title = { Inferring Definite Counterexamples Through
Under-Approximation },
booktitle = { NASA Formal Methods },
year = { 2012 },
series = { Lecture Notes in Computer Science },
publisher = { Springer },
publishedas = { Druck },
language = { eng },
volume = { 7226 },
isbn = { 978-3-642-28890-6 },
pages = { 54--69 },
timestamp = { 2012.01.24 },
i11projectkey = { Arcade },
i11key = { conference },
url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bs12.pdf },
for_reporting_period = { 2012 },
}
-
-
Biallas, S., Kowalewski, S., and Schlich, B., "Leistungsfähige Verifikation von industriellen SPS-Programmen mittels Model-Checking und statischer Analyse", in Proc. AUTOMATION 2011, Baden-Baden, Germany, Düsseldorf, 2011 in VDI-Berichte, VDI-Verlag, pp. 67-72.
Leistungsf{\"a}hige Verifikation von industriellen SPS-Programmen mittels Model-Checking und statischer Analyse
Bibtex entry :
@inproceedings { BKS11,
address = { D{\"u}sseldorf },
author = { Biallas, Sebastian and Kowalewski, Stefan and Schlich,
Bastian },
title = { Leistungsf{\"a}hige Verifikation von industriellen
SPS-Programmen mittels Model-Checking und statischer Analyse },
booktitle = { AUTOMATION 2011, Baden-Baden, Germany },
isbn = { 978-3-18-092143-3 },
issn = { 0083-5560 },
number = { 2143 },
pages = { 67--72 },
publisher = { VDI-Verlag },
publishedas = { Druck },
series = { VDI-Berichte },
language = { eng },
year = { 2011 },
timestamp = { 2011.04.20 },
i11key = { conference },
i11projectkey = { Arcade },
for_reporting_period = { 2011 },
}
-
-
Brauer, J., King, A., and Kriener, J., "Existential Quantification as Incremental SAT", in Proc. Computer Aided Verification (CAV 2011), 2011, vol. 6806 in Lecture Notes in Computer Science, Springer, pp. 191-207.
Existential Quantification as Incremental SAT
Bibtex entry :
@inproceedings { BKK11a,
author = { Brauer, J{\"o}rg and King, Andy and Kriener, Jael },
title = { Existential Quantification as Incremental SAT },
booktitle = { Computer Aided Verification (CAV 2011) },
pages = { 191-207 },
volume = { 6806 },
series = { Lecture Notes in Computer Science },
editor = { Gopalakrishnan, Ganesh and Qadeer, Shaz },
publisher = { Springer },
issn = { 0302-9743 },
isbn = { 978-3-642-22110-1 },
i11key = { conference },
timestamp = { 2011.03.22 },
year = { 2011 },
url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bkk11a.pdf },
language = { eng },
publishedas = { Druck Online },
i11projectkey = { Arcade },
for_reporting_period = { 2011 },
}
-
-
Biallas, S., Brauer, J., and Kowalewski, S., "SAT-Based Abstraction Refinement for Programmable Logic Controllers", in Proc. Dependable Control of Discrete Systems (DCDS'11), 2011, IEEE, pp. 96-101.
SAT-Based Abstraction Refinement for Programmable Logic Controllers
Bibtex entry :
@inproceedings { BBK11,
author = { Biallas, Sebastian and Brauer, J{\"o}rg and Kowalewski,
Stefan },
title = { SAT-Based Abstraction Refinement for Programmable Logic
Controllers },
booktitle = { Dependable Control of Discrete Systems (DCDS'11) },
language = { eng },
publisher = { IEEE },
publishedas = { Druck },
isbn = { 978-1-4244-8969-5 },
pages = { 96--101 },
i11key = { conference },
i11projectkey = { Arcade },
year = { 2011 },
timestamp = { 2011.03.15 },
url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bbk11.pdf },
for_reporting_period = { 2011 },
}
-
-
Brauer, J. and King, A., "Approximate Quantifier Elimination for Propositional Boolean Formulae", in Proc. NASA Formal Methods Symposium (NFM 2011), 2011, vol. 6617 in Lecture Notes in Computer Science, Springer, pp. 73-88.
Approximate Quantifier Elimination for Propositional Boolean Formulae
Bibtex entry :
@inproceedings { BK11b,
author = { Brauer, J{\"o}rg and King, Andy },
title = { Approximate Quantifier Elimination for Propositional Boolean
Formulae },
booktitle = { NASA Formal Methods Symposium (NFM 2011) },
i11key = { conference },
publisher = { Springer },
series = { Lecture Notes in Computer Science },
isbn = { 978-3-642-20397-8 },
pages = { 73--88 },
volume = { 6617 },
year = { 2011 },
timestamp = { 2011.03.04 },
publishedas = { Druck Online },
language = { eng },
url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bk11b.pdf },
i11projectkey = { Arcade },
for_reporting_period = { 2011 },
}
-
-
Schlich, B., Brauer, J., and Kowalewski, S., "Application of Static Analyses for State Space Reduction to Microcontroller Binary Code", Sci. Comput. Program., vol. 76, iss. 2, pp. 100-118, 2011
Application of Static Analyses for State Space Reduction to Microcontroller Binary Code
Bibtex entry :
@article { SBK11,
author = { Schlich, Bastian and Brauer, J{\"o}rg and Kowalewski, Stefan },
title = { Application of Static Analyses for State Space Reduction to
Microcontroller Binary Code },
journal = { Sci. Comput. Program. },
year = { 2011 },
volume = { 76 },
number = { 2 },
pages = { 100--118 },
issn = { 0167-6423 },
url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:sbk10.pdf },
i11key = { journal },
timestamp = { 2010.12.06 },
i11projectkey = { Arcade },
for_reporting_period = { 2011 },
}
-
-
Biallas, S., Brauer, J., Gückel, D., and Kowalewski, S., "On-The-Fly Path Reduction", Electronic Notes in Theoretical Computer Science, vol. 274C, pp. 3-16, 2011, 4th International Workshop on Harnessing Theories for Tool Support in Software (TTSS 2010)
On-The-Fly Path Reduction
Bibtex entry :
@article { BBGK10,
author = { Biallas, Sebastian and Brauer, J{\"o}rg and G{\"u}ckel,
Dominique and Kowalewski, Stefan },
title = { On-The-Fly Path Reduction },
journal = { Electronic Notes in Theoretical Computer Science },
year = { 2011 },
volume = { 274C },
pages = { 3--16 },
publisher = { Elsevier },
note = { 4th International Workshop on Harnessing Theories for Tool
Support in Software (TTSS 2010) },
issn = { 1571-0661 },
i11key = { conference },
i11projectkey = { Arcade },
publishedas = { Online },
language = { eng },
url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bbgk10.pdf },
timestamp = { 2010.10.05 },
for_reporting_period = { 2010 },
}
-
-
Biallas, S., Brauer, J., Kowalewski, S., and Schlich, B., "Automatically Deriving Symbolic Invariants for PLC Programs Written in IL", in Proc. FORMS/FORMAT 2010, 2011, Springer Berlin Heidelberg, pp. 237-245.
Automatically Deriving Symbolic Invariants for {PLC} Programs Written in {IL}
Bibtex entry :
@inproceedings { BBKS10,
author = { Biallas, Sebastian and Brauer, J{\"o}rg and Kowalewski,
Stefan and Schlich, Bastian },
title = { Automatically Deriving Symbolic Invariants for {PLC}
Programs Written in {IL} },
booktitle = { FORMS/FORMAT 2010 },
editor = { Schnieder, Eckehard and Tarnai, Geza },
publisher = { Springer Berlin Heidelberg },
publishedas = { Druck },
language = { eng },
year = { 2011 },
timestamp = { 2010.08.19 },
isbn = { 978-3-642-14261-1 },
pages = { 237--245 },
url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bbks10.pdf },
i11key = { conference },
i11projectkey = { Arcade },
for_reporting_period = { 2010 },
}
-
-
Biallas, S., Brauer, J., and Kowalewski, S., "Counterexample-guided abstraction refinement for PLCs", in Proc. 5th International Workshop on Systems Software Verification (SSV 2010), Vancouver, Canada, Berkeley, CA, USA, 2010, USENIX Association, pp. 2-12.
Counterexample-guided abstraction refinement for {PLCs}
Bibtex entry :
@inproceedings { BBK10,
author = { Biallas, Sebastian and Brauer, J\"{o}rg and Kowalewski,
Stefan },
title = { Counterexample-guided abstraction refinement for {PLCs} },
booktitle = { 5th International Workshop on Systems Software Verification
(SSV 2010), Vancouver, Canada },
year = { 2010 },
location = { Vancouver, BC, Canada },
pages = { 2--12 },
numpages = { 1 },
publisher = { USENIX Association },
address = { Berkeley, CA, USA },
url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bbk10.pdf },
timestamp = { 2010.07.19 },
i11key = { conference },
i11projectkey = { Arcade },
for_reporting_period = { 2010 },
}
-
-
Brauer, J., Kamin, V., Kowalewski, S., and Noll, T., "Loop Refinement using Octagons and Satisfiability", in Proc. Proceedings of the 5th international conference on Systems software verification, Berkeley, CA, USA, 2010, USENIX Association, pp. 1-9.
Loop Refinement using Octagons and Satisfiability
Bibtex entry :
@inproceedings { BKKN10,
author = { Brauer, J{\"o}rg and Kamin, Volker and Kowalewski, Stefan
and Noll, Thomas },
title = { Loop Refinement using Octagons and Satisfiability },
booktitle = { Proceedings of the 5th international conference on Systems
software verification },
year = { 2010 },
location = { Vancouver, BC, Canada },
pages = { 1--9 },
timestamp = { 2010.07.19 },
publisher = { USENIX Association },
address = { Berkeley, CA, USA },
url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bkkn10.pdf },
i11key = { conference },
i11projectkey = { Arcade },
for_reporting_period = { 2010 },
}
-
-
Brauer, J., King, A., and Kowalewski, S., "Range Analysis of Microcontroller Code using Bit-Level Congruences", in Proc. Formal Methods for Industrial Critical Systems (FMICS 2010), Antwerp, Belgium, 2010, vol. 6371 in Lecture Notes in Computer Science, Springer, pp. 82-98.
Range Analysis of Microcontroller Code using Bit-Level Congruences
Bibtex entry :
@inproceedings { BKK10,
author = { Brauer, J{\"o}rg and King, Andy and Kowalewski, Stefan },
title = { Range Analysis of Microcontroller Code using Bit-Level
Congruences },
booktitle = { Formal Methods for Industrial Critical Systems (FMICS 2010),
Antwerp, Belgium },
publisher = { Springer },
series = { Lecture Notes in Computer Science },
year = { 2010 },
volume = { 6371 },
pages = { 82--98 },
timestamp = { 2010.06.08 },
url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bkk10.pdf },
i11key = { conference },
i11projectkey = { Arcade },
for_reporting_period = { 2010 },
}
-
-
Gückel, D., Brauer, J., and Kowalewski, S., "A System for Synthesizing Abstraction-Enabled Simulators for Binary Code Verification", in Proc. Industrial Embedded Systems (SIES 2010), Trento, Italy, 2010, IEEE, pp. 118-127.
A System for Synthesizing Abstraction-Enabled Simulators for Binary Code Verification
Bibtex entry :
@inproceedings { GBK10,
author = { G{\"u}ckel, Dominique and Brauer, J{\"o}rg and Kowalewski,
Stefan },
booktitle = { Industrial Embedded Systems (SIES 2010), Trento, Italy },
title = { A System for Synthesizing Abstraction-Enabled Simulators for
Binary Code Verification },
year = { 2010 },
pages = { 118--127 },
publisher = { IEEE },
timestamp = { 2010.06.01 },
url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:gbk10.pdf },
i11key = { conference },
i11projectkey = { Arcade },
for_reporting_period = { 2010 },
}
-
-
Brauer, J. and King, A., "Automatic Abstraction for Intervals using Boolean Formulae", in Proc. Static Analysis Symposium (SAS 2010), Perpignan, France, 2010, vol. 6337 in Lecture Notes in Computer Science, Springer, pp. 167-183.
Automatic Abstraction for Intervals using Boolean Formulae
Bibtex entry :
@inproceedings { BK10,
author = { Brauer, J{\"o}rg and King, Andy },
title = { Automatic Abstraction for Intervals using Boolean Formulae },
booktitle = { Static Analysis Symposium (SAS 2010), Perpignan, France },
publisher = { Springer },
series = { Lecture Notes in Computer Science },
year = { 2010 },
volume = { 6337 },
pages = { 167--183 },
timestamp = { 2010.05.04 },
url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bk10.pdf },
i11key = { conference },
i11projectkey = { Arcade },
for_reporting_period = { 2010 },
}
-
-
Brauer, J., Noll, T., and Schlich, B., "Interval Analysis of Microcontroller Code using Abstract Interpretation of Hardware and Software", in Proc. Proceedings of the 13th International Workshop on Software and Compilers for Embedded Systems (SCOPES 2010), 2010, ACM.
Interval Analysis of Microcontroller Code using Abstract Interpretation of Hardware and Software
Bibtex entry :
@inproceedings { BNS10,
author = { Brauer, J{\"o}rg and Noll, Thomas and Schlich, Bastian },
title = { Interval Analysis of Microcontroller Code using Abstract
Interpretation of Hardware and Software },
booktitle = { Proceedings of the 13th International Workshop on Software
and Compilers for Embedded Systems (SCOPES 2010) },
year = { 2010 },
publisher = { ACM },
url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:BNS10.pdf },
timestamp = { 2010.04.01 },
i11key = { conference },
i11projectkey = { Arcade },
for_reporting_period = { 2010 },
}
-
-
Gückel, D., Schlich, B., Brauer, J., and Kowalewski, S., "Synthesizing Simulators for Model Checking Microcontroller Binary Code", in Proc. Proceedings of the 13th IEEE International Symposium on Design and Diagnostics of Electronic Circuits and Systems (DDECS 2010), 2010, IEEE, pp. 313-316.
Synthesizing Simulators for Model Checking Microcontroller Binary Code
Bibtex entry :
@inproceedings { GSBK10,
author = { G{\"u}ckel, Dominique and Schlich, Bastian and Brauer,
J{\"o}rg and Kowalewski, Stefan },
title = { Synthesizing Simulators for Model Checking Microcontroller
Binary Code },
booktitle = { Proceedings of the 13th IEEE International Symposium on
Design and Diagnostics of Electronic Circuits and Systems
(DDECS 2010) },
year = { 2010 },
publisher = { IEEE },
pages = { 313--316 },
owner = { gueckel },
i11key = { conference },
url = { http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=5491761 },
timestamp = { 2010.03.08 },
i11projectkey = { Arcade },
for_reporting_period = { 2010 },
}
-
-
Biallas, S., Frey, G., Kowalewski, S., Schlich, B., and Soliman, D., "Formale Verifikation von Sicherheits-Funktionsbausteinen der PLCopen auf Modell- und Code-Ebene", in Proc. Tagungsband Entwicklung und Betrieb komplexer Automatisierungssysteme (EKA 2010), 2010, ifak Magdeburg, pp. 49-57.
Formale Verifikation von Sicherheits-Funktionsbausteinen der PLCopen auf Modell- und Code-Ebene
Bibtex entry :
@inproceedings { BFK+10,
author = { Biallas, Sebastian and Frey, Georg and Kowalewski, Stefan
and Schlich, Bastian and Soliman, Doaa },
title = { Formale Verifikation von Sicherheits-Funktionsbausteinen der
PLCopen auf Modell- und Code-Ebene },
booktitle = { Tagungsband Entwicklung und Betrieb komplexer
Automatisierungssysteme (EKA 2010) },
publisher = { ifak Magdeburg },
publishedas = { Druck },
language = { ger },
pages = { 49--57 },
year = { 2010 },
isbn = { 978-3-940961-41-9 },
location = { Magdeburg, Germany },
i11key = { conference },
i11projectkey = { Arcade },
for_reporting_period = { 2010 },
}
-
-
Brauer, J., Schlich, B., and Kowalewski, S., "Parallel and Distributed Invariant Checking of Microcontroller Software", Electronic Notes in Theoretical Computer Science, vol. 254, p. 45, 2009, Proceedings of the 4th International Workshop on Systems Software Verification (SSV 2009)
Parallel and Distributed Invariant Checking of Microcontroller Software
Bibtex entry :
@article { BSK09b,
title = { Parallel and Distributed Invariant Checking of
Microcontroller Software },
journal = { Electronic Notes in Theoretical Computer Science },
volume = { 254 },
pages = { 45–63 },
year = { 2009 },
note = { Proceedings of the 4th International Workshop on Systems
Software Verification (SSV 2009) },
publisher = { Elsevier },
issn = { 1571-0661 },
author = { Brauer, J{\"o}rg and Schlich, Bastian and Kowalewski, Stefan },
url = { http://portal.acm.org/citation.cfm?id=1630177.1630457 },
i11key = { conference },
i11projectkey = { Arcade },
for_reporting_period = { Old },
}