[BSK+15]
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 : 16. Branchentreff der Mess- und Automatisierungstechnik, 11. und 12. Juni 2015, Baden-Baden / VDI/VDE-Gesellschaft Mess- und Automatisierungstechnik, Düsseldorf, 2015 in VDI-Berichte, VDI-Verl., pp. 95-106.
Automatische Testfallgenerierung für SPS-Programme mittels Zeilenü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 : 16. Branchentreff der Mess- und
Automatisierungstechnik, 11. und 12. Juni 2015, Baden-Baden
/ VDI/VDE-Gesellschaft Mess- und Automatisierungstechnik },
publisher = { VDI-Verl. },
pages = { 95-106 },
series = { VDI-Berichte },
year = { 2015 },
address = { D{\"u}sseldorf },
organization = { AUTOMATION 2015, Baden Baden (Germany), 2015-06-11 -
2015-06-12 },
typ = { PUB:(DE-HGF)7 },
reportid = { RWTH-CONV-207912 },
cin = { 122810 / 120000 },
url = { http://publications.embedded.rwth-aachen.de/file/5r },
}
[HBS+15]
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 : 20th international symposium, Oslo, Norway, June 24 - 26, 2015 ; proceedings / Nikolaj Bjørner; Frank de Boer (eds.), Springer International Publishing, 2015 in Lecture Notes in Computer Science, Cham, pp. 585-588.
Analyzing the Restart Behavior of Industrial Control Applications
Bibtex entry :
@inproceedings { HBS+15,
author = { Hauck-Stattelmann, Stefan and Biallas, Sebastian and
Schlich, Bastian and Kowalewski, Stefan and Jetley, Raoul },
title = { Analyzing the Restart Behavior of Industrial Control
Applications },
booktitle = { FM 2015: formal methods : 20th international symposium,
Oslo, Norway, June 24 - 26, 2015 ; proceedings / Nikolaj
Bjørner; Frank de Boer (eds.) },
publisher = { Cham },
pages = { 585-588 },
series = { Lecture Notes in Computer Science },
year = { 2015 },
address = { Springer International Publishing },
organization = { 20. International Symposium Formal Methods, Oslo (Norway),
2015-06-24 - 2015-06-26 },
doi = { 10.1007/978-3-319-19249-9_38 },
typ = { PUB:(DE-HGF)7 },
reportid = { RWTH-CONV-207691 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/541096 },
}
[SFB+15]
Simon, H., Friedrich, N., Biallas, S., Hauck-Stattelmann, S., Schlich, B., and Kowalewski, S., "Automatic test case generation for PLC programs using coverage metrics", in Proc. 2015 IEEE 20th Conference on Emerging Technologies Factory Automation (ETFA) : 8 - 11 Sept. 2015, City of Luxembourg, Luxembourg / co-sponsored by IEEE ..., Piscataway, NJ, 2015, IEEE, p. 4.
Automatic test case generation for PLC programs using coverage metrics
Bibtex entry :
@inproceedings { SFB+15,
author = { Simon, Hendrik and Friedrich, Nico and Biallas, Sebastian
and Hauck-Stattelmann, Stefan and Schlich, Bastian and
Kowalewski, Stefan },
title = { Automatic test case generation for PLC programs using
coverage metrics },
booktitle = { 2015 IEEE 20th Conference on Emerging Technologies Factory
Automation (ETFA) : 8 - 11 Sept. 2015, City of Luxembourg,
Luxembourg / co-sponsored by IEEE ... },
publisher = { IEEE },
pages = { 4 S. },
year = { 2015 },
address = { Piscataway, NJ },
organization = { 2015 IEEE 20th Conference on Emerging Technologies Factory
Automation, Luxembourg (Luxembourg), 2015-09-08 - 2015-09-11 },
doi = { 10.1109/ETFA.2015.7301602 },
typ = { PUB:(DE-HGF)7 },
reportid = { RWTH-2015-07849 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/565382 },
}
[BKS+14]
Biallas, S., Kowalewski, S., Stattelmann, S., and Schlich, B., "Efficient Handling of States in Abstract Interpretation of Industrial Programmable Logic Controller Code", in Proc. Discrete Event Systems : [Proc. Proceedings of the 12th International Workshop on Discrete Event Systems, Cachan, France, 2014] / Conference Editor: Lesage, Jean-Jacques, Faure, Jean-Marc, Cury, Jose E. R., Lennartson, Bengt, Cachan, France, 2014, IFAC, pp. 400-405.
Efficient Handling of States in Abstract Interpretation of Industrial Programmable Logic Controller Code
Bibtex entry :
@inproceedings { BKS+14,
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 = { Discrete Event Systems : [Proc. Proceedings of the 12th
International Workshop on Discrete Event Systems, Cachan,
France, 2014] / Conference Editor: Lesage, Jean-Jacques,
Faure, Jean-Marc, Cury, Jose E. R., Lennartson, Bengt },
publisher = { IFAC },
pages = { 400-405 },
year = { 2014 },
address = { Cachan, France },
organization = { Discrete Event Systems : [12th International Workshop on
Discrete Event Systems], Cachan (France), 2014-05-14 -
2014-05-16 },
doi = { 10.3182/20140514-3-FR-4046.00065 },
typ = { PUB:(DE-HGF)8 },
reportid = { RWTH-CONV-205968 },
cin = { 120000 / 122810 },
url = { http://publications.rwth-aachen.de/record/443854 },
}
[SBS+14]
Stattelmann, S., Biallas, S., Schlich, B., and Kowalewski, S., "Applying Static Code Analysis on Industrial Controller Code", in Proc. 2014 IEEE [International Conference on] Emerging Technologies and Factory Automation (ETFA 2014) : Barcelona, Spain, 16 - 19 September 2014 / [co-sponsored by Universitat Politècnica de Catalunya - Barcelona Tech (UPC); IEEE Industrial Electronics Society], Piscataway, NJ, 2014, IEEE, p. 4.
Applying Static Code Analysis on Industrial Controller Code
Bibtex entry :
@inproceedings { SBS+14,
author = { Stattelmann, Stefan and Biallas, Sebastian and Schlich,
Bastian and Kowalewski, Stefan },
title = { Applying Static Code Analysis on Industrial Controller Code },
booktitle = { 2014 IEEE [International Conference on] Emerging
Technologies and Factory Automation (ETFA 2014) : Barcelona,
Spain, 16 - 19 September 2014 / [co-sponsored by Universitat
Politècnica de Catalunya - Barcelona Tech (UPC); IEEE
Industrial Electronics Society] },
publisher = { IEEE },
pages = { 4 Seiten },
year = { 2014 },
address = { Piscataway, NJ },
organization = { 2014 IEEE [International Conference on] Emerging
Technologies and Factory Automation, Barcelona (Spain),
2014-09-16 - 2014-09-19 },
doi = { 10.1109/ETFA.2014.7005254 },
typ = { PUB:(DE-HGF)7 },
reportid = { RWTH-CONV-206434 },
cin = { 120000 / 122810 },
url = { http://publications.rwth-aachen.de/record/444619 },
}
[BKK+13]
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 : 14. Branchentreff der Mess- und Automatisierungstechnik ; Kongresshaus Baden-Baden, 25. und 26. Juni 2013 / VDI/VDE-Gesellschaft Mess- und Automatisierungstechnik, Düsseldorf, 2013 in VDI-Berichte, VDI-Verl., pp. 75-79.
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 },
title = { Verifikation von sicherheitsgerichteten SPS-Programmen mit
Hilfe von Safety-Automaten },
booktitle = { Automation 2013 : 14. Branchentreff der Mess- und
Automatisierungstechnik ; Kongresshaus Baden-Baden, 25. und
26. Juni 2013 / VDI/VDE-Gesellschaft Mess- und
Automatisierungstechnik },
publisher = { VDI-Verl. },
pages = { 75-79 },
series = { VDI-Berichte },
year = { 2013 },
address = { D{\"u}sseldorf },
organization = { 14. Branchentreff der Mess- und Automatisierungstechnik
(Germany), 2013-06-25 - 2013-06-26 },
typ = { PUB:(DE-HGF)8 },
reportid = { RWTH-CONV-203699 },
cin = { 120000 / 122810 },
url = { http://publications.rwth-aachen.de/record/226206 },
}
[BKS12]
Biallas, S., Kowalewski, S., and Schlich, B., "Automatische Wertebereichsanalyse von SPS-Programmen", in Proc. Automation 2012 : der 13. Branchentreff der Mess- und Automatisierungstechnik / VDI/VDE-Gesellschaft Mess- und Automatisierungstechnik ; Kongress 'Automation 2012' ; 13 (Baden-Baden) ; 2011.06.13-14Branchentreff der Mess- und Automatisierungstechnik, Düsseldorf, 2012 in VDI-Berichte, VDI-Verl., pp. 79-83.
Automatische Wertebereichsanalyse von SPS-Programmen
Bibtex entry :
@inproceedings { BKS12,
author = { Biallas, Sebastian and Kowalewski, Stefan and Schlich,
Bastian },
title = { Automatische Wertebereichsanalyse von SPS-Programmen },
booktitle = { Automation 2012 : der 13. Branchentreff der Mess- und
Automatisierungstechnik / VDI/VDE-Gesellschaft Mess- und
Automatisierungstechnik ; Kongress 'Automation 2012' ; 13
(Baden-Baden) ; 2011.06.13-14Branchentreff der Mess- und
Automatisierungstechnik },
publisher = { VDI-Verl. },
pages = { 79-83 },
series = { VDI-Berichte },
year = { 2012 },
address = { D{\"u}sseldorf },
organization = { 13. Branchentreff der Mess- und Automatisierungstechnik,
Baden-Baden (Germany), 2011-06-13 - 2011-06-14 },
typ = { PUB:(DE-HGF)8 },
reportid = { RWTH-CONV-191631 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/120638 },
}
[BKS12a]
Biallas, S., Kowalewski, S., and Schlich, B., "Automatische Wertebereichsanalyse -- Formale Verifikation für SPS-Programme", Automatisierungstechnische Praxis : atp, vol. 54, iss. 7/8, pp. 68-74, 2012
Automatische Wertebereichsanalyse -- Formale Verifikation für SPS-Programme
Bibtex entry :
@article { BKS12a,
author = { Biallas, Sebastian and Kowalewski, Stefan and Schlich,
Bastian },
title = { Automatische Wertebereichsanalyse -- Formale Verifikation
f{\"u}r SPS-Programme },
journal = { Automatisierungstechnische Praxis : atp },
publisher = { Oldenbourg Industrieverl. },
pages = { 68-74 },
volume = { 54 },
number = { 7/8 },
year = { 2012 },
address = { M{\"u}nchen },
issn = { 0178-2320 },
typ = { PUB:(DE-HGF)16 },
reportid = { RWTH-CONV-015025 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/133988 },
}
[BKS12b]
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,
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 },
pages = { 378-383 },
year = { 2012 },
address = { Guadalajara, Mexico },
typ = { PUB:(DE-HGF)7 },
reportid = { RWTH-CONV-236327 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/752302 },
}
[BSK12]
Brauer, J., Schlich, B., and Kowalewski, S., "Parallel and distributed invariant checking of microcontroller software", Electronic notes in theoretical computer science : ENTCS, vol. 287, pp. 45-63, 2012
Parallel and distributed invariant checking of microcontroller software
Bibtex entry :
@article { BSK12,
author = { Brauer, J{\"o}rg and Schlich, Bastian and Kowalewski, Stefan },
title = { Parallel and distributed invariant checking of
microcontroller software },
journal = { Electronic notes in theoretical computer science : ENTCS },
publisher = { Elsevier Science },
pages = { 45-63 },
volume = { 287 },
year = { 2012 },
address = { Amsterdam [u.a.] },
issn = { 1571-0661 },
organization = { 4. International Workshop on Numerical and Symbolic Abstract
Domains (France), 10-09-2010 },
doi = { 10.1016/j.entcs.2009.09.059 },
typ = { PUB:(DE-HGF)16 },
reportid = { RWTH-CONV-013643 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/132534 },
}
[BBK+11]
Biallas, S., Brauer, J., Kowalewski, S., and Schlich, B., "Automatically Deriving Symbolic Invariants for PLC Programs Written in IL", in Proc. Formal methods for automation and safety in railway and automotive systems : FORMS/FORMAT 2010 ; [8th symposium ; proceedings] / Eckehard Schnieder; Géza Tarnai, eds., Heidelberg [u.a.], 2011, Springer, pp. 237-245.
Automatically Deriving Symbolic Invariants for PLC Programs Written in IL
Bibtex entry :
@inproceedings { BBK+11,
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 = { Formal methods for automation and safety in railway and
automotive systems : FORMS/FORMAT 2010 ; [8th symposium ;
proceedings] / Eckehard Schnieder; Géza Tarnai, eds. },
publisher = { Springer },
pages = { 237-245 },
year = { 2011 },
address = { Heidelberg [u.a.] },
organization = { Formal methods for automation and safety in railway and
automotive systems, 2010 },
doi = { 10.1007/978-3-642-14261-1 },
typ = { PUB:(DE-HGF)8 },
reportid = { RWTH-CONV-196797 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/126461 },
}
[BKS11]
Biallas, S., Kowalewski, S., and Schlich, B., "Leistungsfähige Verifikation von industriellen SPS-Programmen mittels Model-Checking und statischer Analyse", in Proc. 'Zukunft verantwortungsvoll gestalten' : Automation 2011 ; der 12. Branchentreff der Mess- und Automatisierungstechnik ; Kongress Baden-Baden, 28. und 29. Juni 2011 / VDI/VDE-Gesellschaft Mess- und Automatisierungstechnik. [Kongressleiter: Peter Adolphs ...], Düsseldorf, 2011 in VDI-Berichte, VDI-Verl., pp. 67-72.
Leistungsfähige Verifikation von industriellen SPS-Programmen mittels Model-Checking und statischer Analyse
Bibtex entry :
@inproceedings { BKS11,
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 = { 'Zukunft verantwortungsvoll gestalten' : Automation 2011 ;
der 12. Branchentreff der Mess- und Automatisierungstechnik
; Kongress Baden-Baden, 28. und 29. Juni 2011 /
VDI/VDE-Gesellschaft Mess- und Automatisierungstechnik.
[Kongressleiter: Peter Adolphs ...] },
publisher = { VDI-Verl. },
pages = { 67-72 },
series = { VDI-Berichte },
year = { 2011 },
address = { D{\"u}sseldorf },
organization = { 12. Branchentreff der Mess- und Automatisierungstechnik,
Baden-Baden (Germany), 2011-06-28 - 2011-06-29 },
typ = { PUB:(DE-HGF)8 },
reportid = { RWTH-CONV-189475 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/118212 },
}
[RHS+11]
Reinbacher, T., Horauer, M., Schlich, B., Brauer, J., and Scheuer, F., "Model checking embedded software of an industrial knitting machine", International journal of information technology, communications and convergence, vol. 1, iss. 2, pp. 186-205, 2011
Model checking embedded software of an industrial knitting machine
Bibtex entry :
@article { RHS+11,
author = { Reinbacher, Thomas and Horauer, Martin and Schlich, Bastian
and Brauer, J{\"o}rg and Scheuer, Florian },
title = { Model checking embedded software of an industrial knitting
machine },
journal = { International journal of information technology,
communications and convergence },
publisher = { Inderscience Publishers },
pages = { 186-205 },
volume = { 1 },
number = { 2 },
year = { 2011 },
address = { Geneva },
issn = { 2042-3217 },
doi = { 10.1504/IJITCC.2011.039285 },
typ = { PUB:(DE-HGF)16 },
reportid = { RWTH-CONV-052838 },
cin = { 122810 / 120000 },
url = { http://www.inderscience.com/IJITCC },
}
[SBK11]
Schlich, B., Brauer, J., and Kowalewski, S., "Application of Static Analyses for State-Space Reduction to the Microcontroller Binary Code", Science of computer programming, vol. 76, iss. 2, pp. 100-118, 2011
Application of Static Analyses for State-Space Reduction to the 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
the Microcontroller Binary Code },
journal = { Science of computer programming },
publisher = { Elsevier },
pages = { 100-118 },
volume = { 76 },
number = { 2 },
year = { 2011 },
address = { Amsterdam [u.a.] },
issn = { 0167-6423 },
doi = { 10.1016/j.scico.2010.03.006 },
typ = { PUB:(DE-HGF)16 },
reportid = { RWTH-CONV-062661 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/186222 },
}
[SNB+11]
Schlich, B., Noll, T., Brauer, J., and Brutschy, L., "Reduction of Interrupt Handler Executions for Model Checking Embedded Software", in Proc. Hardware and software: verification and testing : 5th International Haifa Verification Conference, HCV 2009, Haifa, Israel, October 19-22, 2009 : revised selected papers / Kedar Namjoshi ... (eds.), Heidelberg [u.a.], 2011 in Lecture Notes in Computer Science, Springer.
Reduction of Interrupt Handler Executions for Model Checking Embedded Software
Bibtex entry :
@inproceedings { SNB+11,
author = { Schlich, Bastian and Noll, Thomas and Brauer, J{\"o}rg and
Brutschy, Lucas },
title = { Reduction of Interrupt Handler Executions for Model Checking
Embedded Software },
booktitle = { Hardware and software: verification and testing : 5th
International Haifa Verification Conference, HCV 2009,
Haifa, Israel, October 19-22, 2009 : revised selected papers
/ Kedar Namjoshi ... (eds.) },
publisher = { Springer },
series = { Lecture Notes in Computer Science },
year = { 2011 },
address = { Heidelberg [u.a.] },
organization = { 5. International Haifa Verification Conference, HCV 2009,
Haifa (Israel), 2009-10-19 - 2009-10-22 },
doi = { 10.1007/978-3-642-19237-1_5 },
typ = { PUB:(DE-HGF)8 },
reportid = { RWTH-CONV-187757 },
cin = { 122810 / 121310 / 120000 },
url = { http://publications.rwth-aachen.de/record/116214 },
}
[BFK+10]
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. Entwurf komplexer Automatisierungssysteme : EKA 2010 ; Beschreibungsmittel, Methoden, Werkzeuge und Anwendungen ; 11. Fachtagung mit Tutorium, 25. bis 27. Mai 2010 in Magdeburg, Denkfabrik im Wissenschaftshafen / ifak, Institut für Automation und Kommunikation e.V., Magdeburg; Otto-von-Guericke-Universität Magdeburg, Institut für Automatisierungstechnik. [Hrsg.: Ulrich Jumar, Eckehard Schnieder, Christian Diedrich], Magdeburg, 2010, ifak, 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 = { Entwurf komplexer Automatisierungssysteme : EKA 2010 ;
Beschreibungsmittel, Methoden, Werkzeuge und Anwendungen ;
11. Fachtagung mit Tutorium, 25. bis 27. Mai 2010 in
Magdeburg, Denkfabrik im Wissenschaftshafen / ifak, Institut
f{\"u}r Automation und Kommunikation e.V., Magdeburg;
Otto-von-Guericke-Universit{\"a}t Magdeburg, Institut
f{\"u}r Automatisierungstechnik. [Hrsg.: Ulrich Jumar,
Eckehard Schnieder, Christian Diedrich] },
publisher = { ifak },
pages = { 49-57 },
year = { 2010 },
address = { Magdeburg },
organization = { Entwurf komplexer Automatisierungssysteme :
Beschreibungsmittel, Methoden, Werkzeuge und Anwendungen,
Magdeburg (Germany), 2010-05-25 - 2010-05-27 },
typ = { PUB:(DE-HGF)8 },
reportid = { RWTH-CONV-190099 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/118924 },
}
[BNS10]
Brauer, J., Noll, T., and Schlich, B., "Interval Analysis of Microcontroller Code using Abstract Interpretation of Hardware and Software", in Proc. SCOPES '10 Proceedings of the 13th International Workshop on Software & Compilers for Embedded Systems : St. Goar, Germany - June 29-30, 2010, New York, NY, 2010 in ACM Digital Library, 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 = { SCOPES '10 Proceedings of the 13th International Workshop on
Software & Compilers for Embedded Systems : St. Goar,
Germany - June 29-30, 2010 },
publisher = { ACM },
series = { ACM Digital Library },
year = { 2010 },
address = { New York, NY },
organization = { 13. International Workshop on Software & Compilers for
Embedded Systems, St. Goar (Germany), 2010-06-29 -
2010-06-30 },
doi = { 10.1145/1811212.1811216 },
typ = { PUB:(DE-HGF)8 },
reportid = { RWTH-CONV-191119 },
cin = { 122810 / 121310 / 120000 },
url = { http://publications.rwth-aachen.de/record/120063 },
}
[GSB+10]
Gückel, D., Schlich, B., Brauer, J., and Kowalewski, S., "Synthesizing Simulators for Model Checking Microcontroller Binary", in Proc. Proceedings of the 13th IEEE Symposium on Design and Diagnostics of Electronic Circuits and Systems : April 14–16, 2010, Vienna, Austria / Sponsored by IEEE Computer Society, Test Technology Techn. Council, In coop. with Dept. of Computer Engineering, Fac. of Informatics, Vienna Univ. of Techn., Piscataway, NJ, 2010, IEEE, pp. 313-316.
Synthesizing Simulators for Model Checking Microcontroller Binary
Bibtex entry :
@inproceedings { GSB+10,
author = { G{\"u}ckel, Dominique and Schlich, Bastian and Brauer,
J{\"o}rg and Kowalewski, Stefan },
title = { Synthesizing Simulators for Model Checking Microcontroller
Binary },
booktitle = { Proceedings of the 13th IEEE Symposium on Design and
Diagnostics of Electronic Circuits and Systems : April
14–16, 2010, Vienna, Austria / Sponsored by IEEE Computer
Society, Test Technology Techn. Council, In coop. with Dept.
of Computer Engineering, Fac. of Informatics, Vienna Univ.
of Techn. },
publisher = { IEEE },
pages = { 313-316 },
year = { 2010 },
address = { Piscataway, NJ },
organization = { 13. IEEE Symposium on Design and Diagnostics of Electronic
Circuits and Systems, Vienna (Austria), 2010-04-14 -
2010-04-16 },
doi = { 10.1109/DDECS.2010.5491761 },
typ = { PUB:(DE-HGF)8 },
reportid = { RWTH-CONV-190385 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/119227 },
}
[Sch10]
Schlich, B., "Model Checking of Software for Microcontrollers", ACM transactions on embedded computing systems : TECS, vol. 9, iss. 4, p. 27, 2010
Model Checking of Software for Microcontrollers
Bibtex entry :
@article { Sch10,
author = { Schlich, Bastian },
title = { Model Checking of Software for Microcontrollers },
journal = { ACM transactions on embedded computing systems : TECS },
publisher = { ACM Press },
pages = { 27 S. },
volume = { 9 },
number = { 4 },
year = { 2010 },
address = { New York, NY },
issn = { 1539-9087 },
doi = { 10.1145/1721695.1721702 },
typ = { PUB:(DE-HGF)16 },
reportid = { RWTH-CONV-047530 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/169982 },
}
[BHS09]
Brauer, J., Huuck, R., and Schlich, B., "Interprocedural pointer analysis in Goanna", Electronic notes in theoretical computer science : ENTCS, vol. 254, pp. 65-83, 2009
Interprocedural pointer analysis in Goanna
Bibtex entry :
@article { BHS09,
author = { Brauer, J{\"o}rg and Huuck, Ralf and Schlich, Bastian },
title = { Interprocedural pointer analysis in Goanna },
journal = { Electronic notes in theoretical computer science : ENTCS },
publisher = { Elsevier Science },
pages = { 65-83 },
volume = { 254 },
year = { 2009 },
address = { Amsterdam [u.a.] },
issn = { 1571-0661 },
doi = { 10.1016/j.entcs.2009.09.060 },
typ = { PUB:(DE-HGF)16 },
reportid = { RWTH-CONV-013641 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/132532 },
}
[BSR+09]
Brauer, J., Schlich, B., Reinbacher, T., and Kowalewski, S., "Stack bounds analysis of microcontroller assembly code", in Proc. Embedded Systems Week 2009 : CODES+ISSS’09, CASES’09, EMSOFT’09 ; Proceedings of the 2009 international conference on Compilers, architecture, and synthesis for embedded systems ; 2009, Grenoble, France, October 11 - 16, 2009, New York, NY, 2009, ACM Press.
Stack bounds analysis of microcontroller assembly code
Bibtex entry :
@inproceedings { BSR+09,
author = { Brauer, J{\"o}rg and Schlich, Bastian and Reinbacher, Thomas
and Kowalewski, Stefan },
title = { Stack bounds analysis of microcontroller assembly code },
booktitle = { Embedded Systems Week 2009 : CODES+ISSS’09, CASES’09,
EMSOFT’09 ; Proceedings of the 2009 international
conference on Compilers, architecture, and synthesis for
embedded systems ; 2009, Grenoble, France, October 11 - 16,
2009 },
publisher = { ACM Press },
year = { 2009 },
address = { New York, NY },
organization = { 2009 international conference on Compilers, architecture,
and synthesis for embedded systems, Grenoble (France),
2009-10-11 - 2009-10-16 },
doi = { 10.1145/1631716.1631721 },
typ = { PUB:(DE-HGF)8 },
reportid = { RWTH-CONV-173253 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/100433 },
}
[FHS+09]
Fehnker, A., Huuck, R., Schlich, B., and Tapp, M., "Automatic bug detection in microcontroller software by static program analysis"Berlin [u.a.]: Springer, 2009, vol. 5404, pp. 267-278.
Automatic bug detection in microcontroller software by static program analysis
Bibtex entry :
@inbook { FHS+09,
author = { Fehnker, Ansgar and Huuck, Ralf and Schlich, Bastian and
Tapp, Michael },
title = { Automatic bug detection in microcontroller software by
static program analysis },
booktitle = { SOFSEM 2009: theory and practice of computer science : 35th
Conference on Current Trends in Theory and Practice of
Computer Science, Špindler°uv Mlyń, Czech Republic,
January 24 - 30, 2009 ; proceedings / Mogens Nielsen ...
(eds.) },
publisher = { Springer },
pages = { 267-278 },
volume = { 5404 },
series = { Lecture notes in computer science },
year = { 2009 },
address = { Berlin [u.a.] },
doi = { 10.1007/978-3-540-95891-8_26 },
typ = { PUB:(DE-HGF)7 },
reportid = { RWTH-CONV-095395 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/83459 },
}
[KHS09]
Klein, G., Huuck, R., and Schlich, B., "Operating System Verification", Journal of automated reasoning, vol. 42, iss. 2/4, pp. 123-124, 2009
Operating System Verification
Bibtex entry :
@article { KHS09,
author = { Klein, Gerwin and Huuck, Ralf and Schlich, Bastian },
title = { Operating System Verification },
journal = { Journal of automated reasoning },
publisher = { Springer },
pages = { 123-124 },
volume = { 42 },
number = { 2/4 },
year = { 2009 },
address = { Dordrecht [u.a.] },
issn = { 0168-7433 },
doi = { 10.1007/s10817-009-9126-9 },
typ = { PUB:(DE-HGF)16 },
reportid = { RWTH-CONV-065212 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/188901 },
}
[RBH+09]
Reinbacher, T., Brauer, J., Horauer, M., and Schlich, B., "Refining assembly code static analysis for the Intel MCS-51 microcontroller", in Proc. 2009 IEEE International Symposium on Industrial Embedded Systems (SIES 2009) : Lausanne, Switzerland, 08 - 10 July 2009 / [sponsored by: IEEE Industrial Electronics Society (IES)]), Piscataway, NJ, 2009, IEEE, pp. 161-170.
Refining assembly code static analysis for the Intel MCS-51 microcontroller
Bibtex entry :
@inproceedings { RBH+09,
author = { Reinbacher, Thomas and Brauer, J{\"o}rg and Horauer, Martin
and Schlich, Bastian },
title = { Refining assembly code static analysis for the Intel MCS-51
microcontroller },
booktitle = { 2009 IEEE International Symposium on Industrial Embedded
Systems (SIES 2009) : Lausanne, Switzerland, 08 - 10 July
2009 / [sponsored by: IEEE Industrial Electronics Society
(IES)]) },
publisher = { IEEE },
pages = { 161-170 },
year = { 2009 },
address = { Piscataway, NJ },
organization = { 2009 IEEE International Symposium on Industrial Embedded
Systems, Lausanne (Switzerland), 2009-07-08 - 2009-07-10 },
doi = { 10.1109/SIES.2009.5196212 },
typ = { PUB:(DE-HGF)8 },
reportid = { RWTH-CONV-172391 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/99425 },
}
[RHS+09]
Reinbacher, T., Horauer, M., Schlich, B., Brauer, J., and Scheuer, F., "Model checking assembly code of an industrial knitting machine", in Proc. Proceedings of the 2009 Fourth International Conference on Embedded and Multimedia Computing : EM-Com 2009 : [December 10-12, 2009, Jeju Island, Korea], Piscataway, NJ, 2009, IEEE, p. 8.
Model checking assembly code of an industrial knitting machine
Bibtex entry :
@inproceedings { RHS+09,
author = { Reinbacher, Thomas and Horauer, Martin and Schlich, Bastian
and Brauer, J{\"o}rg and Scheuer, Florian },
title = { Model checking assembly code of an industrial knitting
machine },
booktitle = { Proceedings of the 2009 Fourth International Conference on
Embedded and Multimedia Computing : EM-Com 2009 : [December
10-12, 2009, Jeju Island, Korea] },
publisher = { IEEE },
pages = { 8 S. },
year = { 2009 },
address = { Piscataway, NJ },
organization = { 2009 Fourth International Conference on Embedded and
Multimedia Computing, Jeju Island (South Korea), 2009-12-10
- 2009-12-12 },
doi = { 10.1109/EM-COM.2009.5402986 },
typ = { PUB:(DE-HGF)7 },
reportid = { RWTH-CONV-199048 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/129021 },
}
[RHS09]
Reinbacher, T., Horauer, M., and Schlich, B., "Using 3-valued memory representation for state space reduction in embedded assembly code model checking", in Proc. Proceedings of the 2009 IEEE Symposium on Design and Diagnostics of Electronic Circuits and Systems : April 15-17, 2009, Liberec, Czech Republic / M. Renovell; IEEE Computer Society ..., Piscataway, N.J.], 2009, IEEE, pp. 114-119.
Using 3-valued memory representation for state space reduction in embedded assembly code model checking
Bibtex entry :
@inproceedings { RHS09,
author = { Reinbacher, Thomas and Horauer, Martin and Schlich, Bastian },
title = { Using 3-valued memory representation for state space
reduction in embedded assembly code model checking },
booktitle = { Proceedings of the 2009 IEEE Symposium on Design and
Diagnostics of Electronic Circuits and Systems : April
15-17, 2009, Liberec, Czech Republic / M. Renovell; IEEE
Computer Society ... },
publisher = { IEEE },
pages = { 114-119 },
year = { 2009 },
address = { Piscataway, N.J.] },
organization = { 2009 IEEE Symposium on Design and Diagnostics of Electronic
Circuits and Systems, Liberec (Czech Republic), 2009-04-15 -
2009-04-17 },
doi = { 10.1109/DDECS.2009.5012109 },
typ = { PUB:(DE-HGF)8 },
reportid = { RWTH-CONV-172518 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/99559 },
}
[SBW+09]
Schlich, B., Brauer, J., Wernerus, J., and Kowalewski, S., "Direct Model Checking of PLC Programs in IL", IFAC Proceedings Volumes, vol. 42, iss. 5, pp. 28-33, 2009
Direct Model Checking of PLC Programs in IL
Bibtex entry :
@article { SBW+09,
author = { Schlich, Bastian and Brauer, J{\"o}rg and Wernerus, J{\"o}rg
and Kowalewski, Stefan },
title = { Direct Model Checking of PLC Programs in IL },
journal = { IFAC Proceedings Volumes },
publisher = { Elsevier },
pages = { 28-33 },
volume = { 42 },
number = { 5 },
year = { 2009 },
address = { Amsterdam },
issn = { 1474-6670 },
isbn = { 978-3-902661-44-9 },
organization = { 2. IFAC Workshop on Dependable Control of Discrete Systems,
Bari (Italy), 2009-06-10 - 2009-06-12 },
doi = { 10.3182/20090610-3-IT-4004.00010 },
typ = { PUB:(DE-HGF)16 },
reportid = { RWTH-CONV-236337 },
cin = { 122810 / 120000 },
url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:SBWK09.pdf },
}
[SK09]
Schlich, B. and Kowalewski, S., "Model checking C source code for embedded systems", International journal on software tools for technology transfer : STTT, vol. 11, iss. 3, pp. 187-202, 2009
Model checking C source code for embedded systems
Bibtex entry :
@article { SK09,
author = { Schlich, Bastian and Kowalewski, Stefan },
title = { Model checking C source code for embedded systems },
journal = { International journal on software tools for technology
transfer : STTT },
publisher = { Springer },
pages = { 187-202 },
volume = { 11 },
number = { 3 },
year = { 2009 },
address = { Berlin [u.a.] },
issn = { 1433-2779 },
doi = { 10.1007/s10009-009-0106-5 },
typ = { PUB:(DE-HGF)16 },
reportid = { RWTH-CONV-013187 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/132064 },
}
[SKW09]
Schlich, B., Kowalewski, S., and Wernerus, J., "Verifikation von SPS-Programmen in AWL mit Hilfe von direktem Model-Checking", in Proc. Automation 2009 : der Automatisierungskongress in Deutschland ; Kongress Baden-Baden, 16. und 17. Juni 2009 ; [10. Branchentreff der Mess- und Automatisierungstechnik] / VDI/VDE-Gesellschaft Mess- und Automatisierungstechnik. - 2067, Düsseldorf, 2009 in VDI-Berichte, VDI-Verl., pp. 13-16.
Verifikation von SPS-Programmen in AWL mit Hilfe von direktem Model-Checking
Bibtex entry :
@inproceedings { SKW09,
author = { Schlich, Bastian and Kowalewski, Stefan and Wernerus,
J{\"o}rg },
title = { Verifikation von SPS-Programmen in AWL mit Hilfe von
direktem Model-Checking },
booktitle = { Automation 2009 : der Automatisierungskongress in
Deutschland ; Kongress Baden-Baden, 16. und 17. Juni 2009 ;
[10. Branchentreff der Mess- und Automatisierungstechnik] /
VDI/VDE-Gesellschaft Mess- und Automatisierungstechnik. -
2067 },
publisher = { VDI-Verl. },
pages = { 13-16 },
series = { VDI-Berichte },
year = { 2009 },
address = { D{\"u}sseldorf },
organization = { 10. Branchentreff der Mess- und Automatisierungstechnik,
Baden-Baden (Germany), 2009-06-16 - 2009-06-17 },
typ = { PUB:(DE-HGF)8 },
reportid = { RWTH-CONV-172091 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/99088 },
}
[BKK+08]
Beckers, J., Klünder, D., Kowalewski, S., and Schlich, B., "Direct support for model checking abstract state machines by utilizing simulation"Berlin [u.a.]: Springer, 2008, vol. 5238, pp. 112-124.
Direct support for model checking abstract state machines by utilizing simulation
Bibtex entry :
@inbook { BKK+08,
author = { Beckers, J{\"o}rg and Kl{\"u}nder, Daniel and Kowalewski,
Stefan and Schlich, Bastian },
title = { Direct support for model checking abstract state machines by
utilizing simulation },
booktitle = { Abstract state machines, B and Z : first international
conference, ABZ 2008, London, UK, September 16-18, 2008 ;
proceedings / Egon B{\"o}rger ... (eds.) },
publisher = { Springer },
pages = { 112-124 },
volume = { 5238 },
series = { Lecture Notes in Computer Science },
year = { 2008 },
address = { Berlin [u.a.] },
doi = { 10.1007/978-3-540-87603-8_10 },
typ = { PUB:(DE-HGF)7 },
reportid = { RWTH-CONV-095396 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/83460 },
}
[HSW+08]
Herberich, G., Schlich, B., Weise, C., and Noll, T., "Proving correctness of an efficient abstraction for interrupt handling", Electronic notes in theoretical computer science : ENTCS, vol. 217, pp. 133-150, 2008
Proving correctness of an efficient abstraction for interrupt handling
Bibtex entry :
@article { HSW+08,
author = { Herberich, Gerlind and Schlich, Bastian and Weise, Carsten
and Noll, Thomas },
title = { Proving correctness of an efficient abstraction for
interrupt handling },
journal = { Electronic notes in theoretical computer science : ENTCS },
publisher = { Elsevier Science },
pages = { 133-150 },
volume = { 217 },
year = { 2008 },
address = { Amsterdam [u.a.] },
issn = { 1571-0661 },
doi = { 10.1016/j.entcs.2008.06.046 },
typ = { PUB:(DE-HGF)16 },
reportid = { RWTH-CONV-012122 },
cin = { 122810 / 121310 / 120000 },
url = { http://publications.rwth-aachen.de/record/130980 },
}
[NS08]
Noll, T. and Schlich, B., "Delayed nondeterminism in model checking embedded systems assembly code"Berlin [u.a.]: Springer, 2008, vol. 4899, pp. 185-201.
Delayed nondeterminism in model checking embedded systems assembly code
Bibtex entry :
@inbook { NS08,
author = { Noll, Thomas and Schlich, Bastian },
title = { Delayed nondeterminism in model checking embedded systems
assembly code },
booktitle = { Hardware and software: verification and testing : third
International Haifa Verification Conference, HVC 2007,
Haifa, Israel, October 23 - 25, 2007 ; proceedings / Karen
Yorav (ed.) },
publisher = { Springer },
pages = { 185-201 },
volume = { 4899 },
series = { Lecture notes in computer science },
year = { 2008 },
address = { Berlin [u.a.] },
doi = { 10.1007/978-3-540-77966-7_16 },
typ = { PUB:(DE-HGF)7 },
reportid = { RWTH-CONV-095397 },
cin = { 120000 / 122810 / 121310 },
url = { http://publications.rwth-aachen.de/record/83461 },
}
[RKH+08]
Reinbacher, T., Kramer, M., Horauer, M., and Schlich, B., "Motivating model checking for embedded systems software", in Proc. 2008 IEEE/ASME International Conference on Mechatronic and Embedded Systems and Applications : MESA ; Beijing, China, 12 - 15 October 2008, Piscataway, NJ, 2008, IEEE, pp. 546-551.
Motivating model checking for embedded systems software
Bibtex entry :
@inproceedings { RKH+08,
author = { Reinbacher, Thomas and Kramer, Michael and Horauer, Martin
and Schlich, Bastian },
title = { Motivating model checking for embedded systems software },
booktitle = { 2008 IEEE/ASME International Conference on Mechatronic and
Embedded Systems and Applications : MESA ; Beijing, China,
12 - 15 October 2008 },
publisher = { IEEE },
pages = { 546-551 },
year = { 2008 },
address = { Piscataway, NJ },
organization = { 2008 IEEE/ASME International Conference on Mechatronic and
Embedded Systems and Applications, Beijing (Peoples R
China), 2008-10-12 - 2008-10-15 },
doi = { 10.1109/MESA.2008.4735653 },
typ = { PUB:(DE-HGF)8 },
reportid = { RWTH-CONV-172092 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/99089 },
}
[RKH+08a]
Reinbacher, T., Kramer, M., Horauer, M., and Schlich, B., "Challenges in embedded model checking : a simulator for the [mc]square model checker", in Proc. 2008 International Symposium on Industrial Embedded Systems : [SIES'2008] ; La Grande Motte, France, 11 - 13 June 2008 / IEEE, Piscataway, NJ, 2008, IEEE, pp. 245-248.
Challenges in embedded model checking : a simulator for the [mc]square model checker
Bibtex entry :
@inproceedings { RKH+08a,
author = { Reinbacher, Thomas and Kramer, Michael and Horauer, Martin
and Schlich, Bastian },
title = { Challenges in embedded model checking : a simulator for the
[mc]square model checker },
booktitle = { 2008 International Symposium on Industrial Embedded Systems
: [SIES'2008] ; La Grande Motte, France, 11 - 13 June 2008 /
IEEE },
publisher = { IEEE },
pages = { 245-248 },
year = { 2008 },
address = { Piscataway, NJ },
organization = { 2008 International Symposium on Industrial Embedded Systems,
La Grande Motte (France), 2008-06-11 - 2008-06-13 },
doi = { 10.1109/SIES.2008.4577709 },
typ = { PUB:(DE-HGF)7 },
reportid = { RWTH-CONV-172528 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/99569 },
}
[Sch08]
Schlich, B., "Model checking of software for microcontrollers", PhD Thesis, Aachen, 2008.
Model checking of software for microcontrollers
Bibtex entry :
@phdthesis { Sch08,
author = { Schlich, Bastian },
othercontributors = { Kowalewski, Stefan },
title = { Model checking of software for microcontrollers },
publisher = { RWTH Aachen, Department of Computer Science },
pages = { IV, 159 S. : graph. Darst. },
series = { Aachener Informatik-Berichte },
year = { 2008 },
address = { Aachen },
typ = { PUB:(DE-HGF)11 },
reportid = { RWTH-CONV-125168 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/63747/files/Schlich_Bastian.pdf },
}
[SGK08]
Schlich, B., Gückel, D., and Kowalewski, S., "Modeling the environment of microcontrollers to tackle the state-explosion problem in model checking", in Proc. Formal methods for automation and safety in railway and automotive systems ; proceedings of Symposium FORMS/FORMAT 2008, Budapest, Hungary, October 9 - 10, 2008 / Géza Tarnai ... (ed.), Budapest, 2008, L Harmattan.
Modeling the environment of microcontrollers to tackle the state-explosion problem in model checking
Bibtex entry :
@inproceedings { SGK08,
author = { Schlich, Bastian and G{\"u}ckel, Dominique and Kowalewski,
Stefan },
title = { Modeling the environment of microcontrollers to tackle the
state-explosion problem in model checking },
booktitle = { Formal methods for automation and safety in railway and
automotive systems ; proceedings of Symposium FORMS/FORMAT
2008, Budapest, Hungary, October 9 - 10, 2008 / Géza Tarnai
... (ed.) },
publisher = { L Harmattan },
year = { 2008 },
address = { Budapest },
organization = { Symposium FORMS/FORMAT 2008, Budapest (Hungary), 2008-10-09
- 2008-10-10 },
typ = { PUB:(DE-HGF)8 },
reportid = { RWTH-CONV-171805 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/98749 },
}
[SLK08]
Schlich, B., Löll, J., and Kowalewski, S., "Application of static analyses for state space reduction to microcontroller assembly code"Berlin [u.a.]: Springer, 2008, vol. 4916, pp. 21-37.
Application of static analyses for state space reduction to microcontroller assembly code
Bibtex entry :
@inbook { SLK08,
author = { Schlich, Bastian and L{\"o}ll, Jann and Kowalewski, Stefan },
title = { Application of static analyses for state space reduction to
microcontroller assembly code },
booktitle = { Formal methods for industrial critical systems : 12th
international workshop, FMICS 2007, Berlin, Germany, July 1
- 2, 2007 ; revised selected papers / Stefan Leue; Pedro
Merino (eds.) },
publisher = { Springer },
pages = { 21-37 },
volume = { 4916 },
series = { Lecture notes in computer science },
year = { 2008 },
address = { Berlin [u.a.] },
doi = { 10.1007/978-3-540-79707-4_4 },
typ = { PUB:(DE-HGF)7 },
reportid = { RWTH-CONV-095398 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/83462 },
}
[SK07d]
Schlich, B. and Kowalewski, S., "An extendable architecture for model checking hardware-specific automotive microcontroller code", in Proc. FORMS/FORMAT 2007 - 6th symposium : formal methods for automation and safety in railway and automotive systems ; proceedings of Symposium FORMS/FORMAT 2007, Braunschweig, Germany, 25th and 26th January, 2007 / Eckehard Schnieder; Géza Tarnai (Eds.), Braunschweig, 2007, GZVB, pp. 202-212.
An extendable architecture for model checking hardware-specific automotive microcontroller code
Bibtex entry :
@inproceedings { SK07d,
author = { Schlich, Bastian and Kowalewski, Stefan },
title = { An extendable architecture for model checking
hardware-specific automotive microcontroller code },
booktitle = { FORMS/FORMAT 2007 - 6th symposium : formal methods for
automation and safety in railway and automotive systems ;
proceedings of Symposium FORMS/FORMAT 2007, Braunschweig,
Germany, 25th and 26th January, 2007 / Eckehard Schnieder;
Géza Tarnai (Eds.) },
publisher = { GZVB },
pages = { 202-212 },
year = { 2007 },
address = { Braunschweig },
organization = { 6. symposium : formal methods for automation and safety in
railway and automotive systems, Braunschweig (Germany),
2007-01-25 - 2007-01-26 },
typ = { PUB:(DE-HGF)8 },
reportid = { RWTH-CONV-188508 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/117067 },
}
[SSK07]
Schlich, B., Salewski, F., and Kowalewski, S., "Applying model checking to an automotive microcontroller application", in Proc. 2007 International Symposium on Industrial Embedded Systems : Costa da Caparica, [Lisbon], Portugal, 4 - 6 July 2007 ; [SIES'2007] / IEEE / IEEE Computer Society Press, Piscataway, NJ, 2007, IEEE, pp. 209-216.
Applying model checking to an automotive microcontroller application
Bibtex entry :
@inproceedings { SSK07,
author = { Schlich, Bastian and Salewski, Falk and Kowalewski, Stefan },
title = { Applying model checking to an automotive microcontroller
application },
booktitle = { 2007 International Symposium on Industrial Embedded Systems
: Costa da Caparica, [Lisbon], Portugal, 4 - 6 July 2007 ;
[SIES'2007] / IEEE / IEEE Computer Society Press },
publisher = { IEEE },
pages = { 209-216 },
year = { 2007 },
address = { Piscataway, NJ },
organization = { International Symposium on Industrial Embedded Systems,
Costa da Caparica (Portugal), 2007-07-04 - 2007-07-06 },
doi = { 10.1109/SIES.2007.4297337 },
typ = { PUB:(DE-HGF)8 },
reportid = { RWTH-CONV-188512 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/117071 },
}
[PSK06]
Palczynski, J., Schlich, B., and Kowalewski, S., "Eine Evaluationssuite zur schnellen Bewertung von Matlab/Simulink-Modelcheckern", in Proc. Informatik 2006 : Informatik für Menschen ; Beiträge der 36. Jahrestagung der Gesellschaft für Informatik e.V. (GI) ; 2. bis 6. Oktober 2006 in Dresden / Christian Hochberger ... (Hrsg.). - T. 1. - 1, Bonn, 2006 in GI-Edition : Proceedings, Ges. für Informatik, pp. 751-755.
Eine Evaluationssuite zur schnellen Bewertung von Matlab/Simulink-Modelcheckern
Bibtex entry :
@inproceedings { PSK06,
author = { Palczynski, Jacob and Schlich, Bastian and Kowalewski,
Stefan },
title = { Eine Evaluationssuite zur schnellen Bewertung von
Matlab/Simulink-Modelcheckern },
booktitle = { Informatik 2006 : Informatik f{\"u}r Menschen ; Beitr{\"a}ge
der 36. Jahrestagung der Gesellschaft f{\"u}r Informatik
e.V. (GI) ; 2. bis 6. Oktober 2006 in Dresden / Christian
Hochberger ... (Hrsg.). - T. 1. - 1 },
publisher = { Ges. f{\"u}r Informatik },
pages = { 751-755 },
series = { GI-Edition : Proceedings },
year = { 2006 },
address = { Bonn },
organization = { 36. Jahrestagung der Gesellschaft f{\"u}r Informatik e.V.,
Dresden (Germany), 2006-10-02 - 2006-10-06 },
typ = { PUB:(DE-HGF)8 },
reportid = { RWTH-CONV-183701 },
cin = { 120000 / 122810 },
url = { http://publications.rwth-aachen.de/record/111754 },
}
[SK06a]
Schlich, B. and Kowalewski, S., "[mc]square: A model checker for microcontroller code", in Proc. ISoLA 2006 : Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation ; 15 - 19 November 2006, Paphos, Cyprus / IEEE Computer SocietyLeveraging Applications of Formal Methods, Verification and Validation (ISoLA 2006), Paphos, Cyprus, 2006, IEEE Computer Society Press, pp. 466-473.
[mc]square: A model checker for microcontroller code
Bibtex entry :
@inproceedings { SK06a,
author = { Schlich, Bastian and Kowalewski, Stefan },
title = { [mc]square: A model checker for microcontroller code },
booktitle = { ISoLA 2006 : Second International Symposium on Leveraging
Applications of Formal Methods, Verification and Validation
; 15 - 19 November 2006, Paphos, Cyprus / IEEE Computer
SocietyLeveraging Applications of Formal Methods,
Verification and Validation (ISoLA 2006) },
publisher = { IEEE Computer Society Press },
pages = { 466-473 },
year = { 2006 },
address = { Paphos, Cyprus },
organization = { 2. International Symposium on Leveraging Applications of
Formal Methods, Verification and Validation, Paphos
(Cyprus), 2006-11-15 - 2006-11-19 },
doi = { 10.1109/ISoLA.2006.62 },
typ = { PUB:(DE-HGF)8 },
reportid = { RWTH-CONV-188517 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/117076 },
}
[SRW+06]
Schlich, B., Rohrbach, M., Weber, M., and Kowalewski, S., "Model checking software for microcontrollers", , Aachen, AIB-2006-11, 2006.
Model checking software for microcontrollers
Bibtex entry :
@techreport { SRW+06,
author = { Schlich, Bastian and Rohrbach, Michael and Weber, Michael
and Kowalewski, Stefan },
title = { Model checking software for microcontrollers },
pages = { 33 Bl. : graph. Darst. },
volume = { 2006,11 },
number = { AIB-2006-11 },
series = { Aachener Informatik-Berichte },
year = { 2006 },
address = { Aachen },
typ = { PUB:(DE-HGF)29 },
reportid = { RWTH-CONV-008343 },
cin = { 122810 / 120000 },
url = { http://webdoc.sub.gwdg.de/ebook/serien/ah/AIB/2006-11.pdf },
}
[SK05b]
Schlich, B. and Kowalewski, S., "Model checking C source code for embedded systems", , [S.l.], NASA/CP-2005-212788, 2005.
Model checking C source code for embedded systems
Bibtex entry :
@techreport { SK05b,
author = { Schlich, Bastian and Kowalewski, Stefan },
title = { Model checking C source code for embedded systems },
booktitle = { IEEE/NASA Workshop on Leveraging Applications of Formal
Methods, Verification, and Validation : IEEE/NASA ISoLA 2005
; proceedings of a workshop held at the Loyola College
Graduate Center, Columbia, Maryland, USA, 23 - 24 September
2005 ; with a special track on the theme of formal methods
in human and robotic space exploration / National
Aeronautics and Space Administration, Goddard Space Flight
Center. Ed.: Tiziana Margaria ... },
pages = { 65-77 },
number = { NASA/CP-2005-212788 },
year = { 2005 },
address = { [S.l.] },
organization = { IEEE/NASA Workshop on Leveraging Applications of Formal
Methods, Verification, and Validation, Columbia (USA),
2005-09-23 - 2005-09-24 },
typ = { PUB:(DE-HGF)8 },
reportid = { RWTH-CONV-009447 },
cin = { 120000 / 122810 },
url = { http://publications.rwth-aachen.de/record/111740 },
}
[SK04]
Schlich, B. and Kowalewski, S., "C Model Checker: Eine Übersicht", 2004.
C Model Checker: Eine Übersicht
Bibtex entry :
@techreport { SK04,
author = { Schlich, Bastian and Kowalewski, Stefan },
title = { C Model Checker: Eine {\"U}bersicht },
year = { 2004 },
typ = { PUB:(DE-HGF)29 },
reportid = { RWTH-CONV-101608 },
cin = { 122810 / 120000 },
url = { http://publications.rwth-aachen.de/record/90178 },
}