% % This file was created by the TYPO3 extension % bib % --- Timezone: CEST % Creation date: 2024-04-20 % Creation time: 16-54-15 % --- Number of references % 19 % @Inproceedings { 2022-schemmel-kdalloc, title = {A Deterministic Memory Allocator for Dynamic Symbolic Execution}, year = {2022}, month = {6}, tags = {safe}, url = {https://drops.dagstuhl.de/opus/volltexte/2022/16237/pdf/LIPIcs-ECOOP-2022-9.pdf}, booktitle = {European Conference on Object-Oriented Programming (ECOOP 2022)}, DOI = {10.4230/LIPIcs.ECOOP.2022.9}, reviewed = {1}, author = {Schemmel, Daniel and B{\"u}ning, Julian and Busse, Frank and Nowack, Martin and Cadar, Cristian} } @Inproceedings { 2020-schemmel-porse, title = {Symbolic Partial-Order Execution for Testing Multi-Threaded Programs}, year = {2020}, month = {7}, tags = {symbiosys}, url = {https://arxiv.org/pdf/2005.06688.pdf}, web_url2 = {https://arxiv.org/abs/2005.06688}, booktitle = {Computer Aided Verification (CAV 2020)}, event_name = {32nd International Conference on Computer Aided Verification}, DOI = {10.1007/978-3-030-53288-8_18}, reviewed = {1}, author = {Schemmel, Daniel and B{\"u}ning, Julian and Rodr{\'i}guez, C{\'e}sar and Laprell, David and Wehrle, Klaus} } @Proceedings { 2018-QuicTesting, title = {Interoperability-Guided Testing of QUIC Implementations using Symbolic Execution}, year = {2018}, month = {12}, day = {4}, tags = {erc,symbiosys}, url = {https://www.comsys.rwth-aachen.de/fileadmin/papers/2018/2018-rath-quictesting.pdf}, web_url = {https://dl.acm.org/citation.cfm?id=3284853}, web_url2 = {https://arxiv.org/abs/1811.12099}, publisher = {ACM}, event_place = {Heraklion, Greece}, event_name = {EPIQ'18 Workshop Paper}, event_date = {4.12.2018}, language = {en}, ISBN = {978-1-4503-6082-1}, DOI = {10.1145/3284850.3284853}, reviewed = {1}, author = {Rath, Felix and Schemmel, Daniel and Wehrle, Klaus} } @Article { 2018-stoffers-on-automated-memoization, title = {On Automated Memoization in the Field of Simulation Parameter Studies}, journal = {ACM Transactions on Modeling and Computer Simulation (TOMACS)}, year = {2018}, month = {10}, volume = {28}, number = {4}, number2 = {Article 26}, pages = {26:1-26:25}, tags = {memosim,symbiosys}, url = {file:2213}, DOI = {10.1145/3186316}, reviewed = {1}, author = {Stoffers, Mirko and Schemmel, Daniel and Soria Dustmann, Oscar and Wehrle, Klaus} } @Inproceedings { 2018-soria-dustmann-parti, title = {PARTI: A Multi-interval Theory Solver for Symbolic Execution}, year = {2018}, month = {9}, tags = {symbiosys}, url = {file:2195}, booktitle = {Proceedings of the 2018 Conference on Automated Software Engineering (ASE'18)}, DOI = {10.1145/3238147.3238179}, reviewed = {1}, author = {Soria Dustmann, Oscar and Wehrle, Klaus and Cadar, Cristian} } @Inproceedings { 2018-cav-schemmel-liveness, title = {Symbolic Liveness Analysis of Real-World Software}, year = {2018}, month = {7}, day = {14}, tags = {symbiosys}, url = {https://www.comsys.rwth-aachen.de/fileadmin/papers/2018/2018-schemmel-symbolic-liveness-analysis-of-real-world-software.pdf}, booktitle = {Computer Aided Verification (CAV 2018)}, event_place = {Oxford, Great Britain}, event_name = {30th International Conference on Computer Aided Verification}, event_date = {2018-07-14 to 2018-07-17}, language = {en}, DOI = {10.1007/978-3-319-96142-2_27}, reviewed = {1}, author = {Schemmel, Daniel and B{\"u}ning, Julian and Soria Dustmann, Oscar and Noll, Thomas and Wehrle, Klaus} } @Inproceedings { 2018-cpsbench-schemmel-equiv, title = {Towards Benchmark Optimization by Automated Equivalence Detection}, year = {2018}, month = {4}, day = {10}, tags = {symbiosys,reflexes}, url = {file:2196}, booktitle = {Proceedings of the 1st Workshop on Benchmarking Cyber-Physical Networks and Systems (CPSBench'18)}, event_place = {Porto, Portugal}, event_name = {1st Workshop on Benchmarking Cyber-Physical Networks and Systems}, event_date = {2018-04-10}, ISBN = {978-1-5386-6742-2}, DOI = {10.1109/CPSBench.2018.00011}, reviewed = {1}, author = {Schemmel, Daniel and Glebke, Ren{\'e} and Stoffers, Mirko and Wehrle, Klaus} } @Inproceedings { 2017-liew-schemmel-fp, title = {Floating-Point Symbolic Execution: A Case Study in N-Version Programming}, year = {2017}, month = {10}, day = {30}, tags = {symbiosys}, url = {file:1848}, booktitle = {Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering}, event_place = {Urbana-Champaign, IL, USA}, language = {en}, ISBN = {978-1-5386-2684-9/17}, reviewed = {1}, author = {Liew, Daniel and Schemmel, Daniel and Cadar, Cristian and Donaldson, Alastair and Z{\"a}hl, Rafael and Wehrle, Klaus} } @Inproceedings { 2017-stoffers-dsrt-memo-ident, title = {Automated Memoization: Automatically Identifying Memoization Units in Simulation Parameter Studies}, year = {2017}, month = {10}, day = {18}, pages = {33-42}, keywords = {Automatic Memoization; Accelerating Parameter Studies; Performance Prediction}, tags = {memosim,symbiosys}, url = {http://www.comsys.rwth-aachen.de/fileadmin/papers/2017/2017-stoffers-dsrt-memo-ident.pdf}, misc2 = {Online}, publisher = {IEEE}, booktitle = {Proceedings of the 21st IEEE/ACM International Symposium on Distributed Simulation and Real Time Applications (DS-RT 2017), Rome, Italy}, event_place = {Rome, Italy}, language = {en}, DOI = {10.1109/DISTRA.2017.8167664}, reviewed = {1}, author = {Stoffers, Mirko and Bettermann, Ralf and Wehrle, Klaus} } @Proceedings { 2017-SymPerfPoster, title = {SymPerf: Predicting Network Function Performance}, year = {2017}, month = {8}, day = {21}, tags = {spp,erc,symbiosys,reflexes}, url = {https://www.comsys.rwth-aachen.de/fileadmin/papers/2017/2017-rath-sym-perf-poster.pdf}, publisher = {ACM}, event_place = {Los Angeles, USA}, event_name = {ACM SIGCOMM 2017 Poster}, event_date = {21.8.2017 - 25.8.2017}, language = {en}, ISBN = {978-1-4503-5057-0/17/08}, DOI = {10.1145/3123878.3131977}, reviewed = {1}, author = {Rath, Felix and Krude, Johannes and R{\"u}th, Jan and Schemmel, Daniel and Hohlfeld, Oliver and Bitsch Link, J{\'o} Agila and Wehrle, Klaus} } @Inproceedings { 2017-serror-pads-cows, title = {Code-transparent Discrete Event Simulation for Time-accurate Wireless Prototyping}, year = {2017}, month = {5}, day = {24}, tags = {memosim,symbiosys}, url = {https://www.comsys.rwth-aachen.de/fileadmin/papers/2017/2017-serror-pads-cows.pdf}, publisher = {ACM}, howpublished = {online}, booktitle = {Proceedings of the 5th ACM SIGSIM/PADS Conference on Principles of Advanced Discrete Simulation (SIGSIM-PADS’17), Singapore, Singapore}, event_place = {Singapore, Singapore}, event_name = {5th ACM SIGSIM/PADS Conference on Principles of Advanced Discrete Simulation (SIGSIM-PADS’17)}, event_date = {May 24-26, 2017}, ISBN = {978-1-4503-4489-0}, DOI = {10.1145/3064911.3064913}, reviewed = {1}, author = {Serror, Martin and Kirchhof, J{\"o}rg Christian and Stoffers, Mirko and Wehrle, Klaus and Gross, James} } @Inproceedings { 2016-stoffers-pads-memo, title = {Automated Memoization for Parameter Studies Implemented in Impure Languages}, year = {2016}, month = {5}, day = {15}, pages = {221-232}, note = {Best Paper Award}, keywords = {Automatic Memoization; Accelerating Parameter Studies; Impure Languages}, tags = {memosim,symbiosys}, url = {http://www.comsys.rwth-aachen.de/fileadmin/papers/2016/2016-stoffers-pads-memoization.pdf}, misc2 = {Online}, publisher = {ACM}, address = {New York, NY}, booktitle = {Proceedings of the 4th ACM SIGSIM/PADS Conference on Principles of Advanced Discrete Simulation (SIGSIM-PADS’16), Banff, AB, Canada}, event_place = {Banff, AB, Canada}, language = {en}, DOI = {10.1145/2901378.2901386}, reviewed = {1}, author = {Stoffers, Mirko and Schemmel, Daniel and Soria Dustmann, Oscar and Wehrle, Klaus} } @Inproceedings { 2012-wripe-sasnauskas-symnet, title = {Integration Testing of Protocol Implementations using Symbolic Distributed Execution}, year = {2012}, month = {10}, pages = {6 S.}, tags = {kleenet}, url = {fileadmin/papers/2012/2012-09-wripe-sasnauskas-SymNet.pdf}, misc2 = {Print Online}, address = {Piscataway, NJ, USA}, booktitle = {The 2nd International Workshop on Rigorous Protocol Engineering (WRiPE 2012), 30 October - 02 November 2012, Austin, TX, USA}, organization = {IEEE}, event_place = {Austin, TX, USA}, event_name = {The 2nd International Workshop on Rigorous Protocol Engineering (WRiPE 2012)}, event_date = {October 30 - November 02 2012}, language = {en}, ISBN = {978-1-4673-2445-8}, DOI = {10.1109/ICNP.2012.6459940}, reviewed = {1}, author = {Sasnauskas, Raimondas and Kaiser, Philipp and Jukić, Russ Lucas and Wehrle, Klaus} } @Inproceedings { 2012-taicpart-dustmann-symbolic-time, title = {Position Paper: Symbolic System Time in Distributed Systems Testing}, year = {2012}, month = {4}, abstract = {We propose an extension of symbolic execution of distributed systems to test software parts related to timing. Currently, the execution model is limited to symbolic input for individual nodes, not capturing the important class of timing errors resulting from varying network conditions. In this paper, we introduce symbolic system time in order to systematically find timing-related bugs in distributed systems. Instead of executing time events at a concrete time, we execute them at a set of times and analyse possible event interleavings on demand. We detail on the resulting problem space, discuss possible algorithmic optimisations, and highlight our future research directions.}, tags = {kleenet}, url = {fileadmin/papers/2012/2012-04-taicpart-soriadustmann-symtime.pdf}, booktitle = {TAICPART'2012}, language = {en}, reviewed = {1}, author = {Soria Dustmann, Oscar and Sasnauskas, Raimondas and Wehrle, Klaus} } @Inproceedings { 2011-icdcs-sasnauskas-sde, title = {Scalable Symbolic Execution of Distributed Systems}, year = {2011}, month = {6}, pages = {333-342}, abstract = {Recent advances in symbolic execution have proposed a number of promising solutions to automatically achieve high-coverage and explore non-determinism during testing. This attractive testing technique of unmodified software assists developers with concrete inputs and deterministic schedules to analyze erroneous program paths. Being able to handle complex systems' software, these tools only consider single software instances and not their distributed execution which forms the core of distributed systems. The step to symbolic distributed execution is however steep, posing two core challenges: (1) additional state growth and (2) the state intra-dependencies resulting from communication. In this paper, we present SDE—a novel approach enabling scalable symbolic execution of distributed systems. The key contribution of our work is two-fold. First, we generalize the problem space of SDE and develop an algorithm significantly eliminating redundant states during testing. The key idea is to benefit from the nodes' local communication minimizing the number of states representing the distributed execution. Second, we demonstrate the practical applicability of SDE in testing with three sensornet scenarios running Contiki OS.}, tags = {kleenet}, url = {fileadmin/papers/2011/2011-06-icdcs-sasnauskas-sde.pdf}, misc2 = {Druck}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, booktitle = {Proceedings of the 31st IEEE International Conference on Distributed Computing Systems (ICDCS 2011), June 2011, Minneapolis, MN, USA}, language = {en}, ISBN = {978-0-7695-4364-2}, ISSN = {1063-6927}, DOI = {10.1109/ICDCS.2011.28}, reviewed = {1}, author = {Sasnauskas, Raimondas and Soria Dustmann, Oscar and Kaminski, Benjamin Lucien and Weise, Carsten and Kowalewski, Stefan and Wehrle, Klaus} } @Inproceedings { 2010-sensys-sasnauskas-coojakleenet, title = {Demo Abstract: Integrating Symbolic Execution with Sensornet Simulation for Efficient Bug Finding}, year = {2010}, month = {11}, pages = {383--384}, abstract = {High-coverage testing of sensornet applications is vital for pre-deployment bug cleansing, but has previously been difficult due to the limited set of available tools. We integrate the KleeNet symbolic execution engine with the COOJA network simulator to allow for straight-forward and intuitive high-coverage testing initiated from a simulation environment. A tight coupling of simulation and testing helps detect, narrow down, and fix complex interaction bugs in an early development phase. We demonstrate the seamless transition between COOJA simulation and KleeNet symbolic execution. Our framework enables future research in how high-coverage testing tools could be used in cooperation with simulation tools.}, tags = {kleenet}, url = {fileadmin/papers/2010/2010-osterlind_sasnauskas-sensys-coojakleenet.pdf}, misc2 = {Print}, publisher = {ACM}, address = {New York, NY, USA}, booktitle = {Proceedings of the 8th ACM Conference on Embedded Networked Sensor Systems (SenSys 2010), Zurich, Switzerland}, language = {en}, ISBN = {978-1-4503-0344-6}, DOI = {http://doi.acm.org/10.1145/1869983.1870034}, reviewed = {1}, author = {{\"O}sterlind, Fredrik and Sasnauskas, Raimondas and Dunkels, Adam and Soria Dustmann, Oscar and Wehrle, Klaus} } @Inproceedings { 2010-ipsn-sasnauskas-kleenet, title = {KleeNet: Discovering Insidious Interaction Bugs in Wireless Sensor Networks Before Deployment}, year = {2010}, month = {4}, day = {12}, pages = {186--196}, abstract = {Complex interactions and the distributed nature of wireless sensor networks make automated testing and debugging before deployment a necessity. A main challenge is to detect bugs that occur due to non-deterministic events, such as node reboots or packet duplicates. Often, these events have the potential to drive a sensor network and its applications into corner-case situations, exhibiting bugs that are hard to detect using existing testing and debugging techniques. In this paper, we present KleeNet, a debugging environment that effectively discovers such bugs before deployment. KleeNet executes unmodified sensor network applications on symbolic input and automatically injects non-deterministic failures. As a result, KleeNet generates distributed execution paths at high-coverage, including low-probability corner-case situations. As a case study, we integrated KleeNet into the Contiki OS and show its effectiveness by detecting four insidious bugs in the uIP TCP/IP protocol stack. One of these bugs is critical and lead to refusal of further connections.}, keywords = {automated protocol testing, experimentation, failure detection, wireless sensor networks}, tags = {kleenet}, url = {fileadmin/papers/2010/2010-04-ipsn-sasnauskas-KleeNet.pdf}, misc2 = {Print}, publisher = {ACM}, address = {New York, NY, USA}, booktitle = {Proceedings of the 9th ACM/IEEE International Conference on Information Processing in Sensor Networks (IPSN 2010), Stockholm, Sweden}, language = {en}, ISBN = {978-1-60558-988-6}, DOI = {http://doi.acm.org/10.1145/1791212.1791235}, reviewed = {1}, author = {Sasnauskas, Raimondas and Landsiedel, Olaf and Alizai, Muhammad Hamad and Weise, Carsten and Kowalewski, Stefan and Wehrle, Klaus} } @Inproceedings { 2008-sensys-sasnauskas-kleenet, title = {Poster Abstract: KleeNet - Automatic Bug Hunting in Sensor Network Applications}, year = {2008}, month = {11}, pages = {425--426}, abstract = {We present KleeNet, a Klee based bug hunting tool for sensor network applications before deployment. KleeNet automatically tests code for all possible inputs, ensures memory safety, and integrates well into TinyOS based application development life cycle, making it easy for developers to test their applications.}, keywords = {bug finding, memory safety, tinyos, type safety}, tags = {kleenet}, url = {fileadmin/papers/2008/2008-11-Sasnauskas-SenSys08-KleeNet.pdf}, misc2 = {Print}, publisher = {ACM}, address = {New York, NY, USA}, booktitle = {Proceedings of the 6th ACM conference on Embedded network sensor systems (SenSys'08), Raleigh, NC, USA}, language = {en}, ISBN = {978-1-59593-990-6}, DOI = {http://doi.acm.org/10.1145/1460412.1460485}, reviewed = {1}, author = {Sasnauskas, Raimondas and Bitsch Link, J{\'o} Agila and Alizai, Muhammad Hamad and Wehrle, Klaus} } @Techreport { 2008-fgsn-sasnauskas-kleenet, title = {Bug Hunting in Sensor Network Applications}, year = {2008}, month = {9}, abstract = {Testing sensor network applications is an essential and a difficult task. Due to their distributed and faulty nature, severe resource constraints, unobservable interactions, and limited human interaction, sensor networks, make monitoring and debugging of applications strenuous and more challenging. In this paper we present KleeNet - a Klee based platform independent bug hunting tool for sensor network applications before deployment - which can automatically test applications for all possible inputs, and hence, ensures memory safety for TinyOS based applications. Upon finding a bug, KleeNet generates a concrete test case with real input values identifying a specific error path in a program. Additionally, we show that KleeNet integrates well into TinyOS application development life cycle with minimum manual effort, making it easy for developers to test their applications.}, tags = {kleenet}, url = {fileadmin/papers/2008/2008-09-Sasnauskas-FGSN08-BugHunting.pdf}, web_url = {ftp://ftp.inf.fu-berlin.de/pub/reports/tr-b-08-12.pdf}, misc2 = {Print}, publisher = {Freie Universit{\"a}t Berlin, Institute of Computer Science}, address = {Berlin, Germany}, booktitle = {Proceedings of the 7th GI/ITG Fachgespraech Wireless Sensor Networks, Berlin, Germany}, institution = {Chair of Communication and Distributed Systems (ComSys)}, language = {en}, reviewed = {1}, author = {Sasnauskas, Raimondas and Bitsch Link, J{\'o} Agila and Alizai, Muhammad Hamad and Wehrle, Klaus} }