Showing 1–15 of 15 results for author: Fischer, B

Mai Ho'omāuna i ka 'Ai: Language Models Improve Automatic Speech Recognition in Hawaiian

Authors: Kaavya Chaparala, Guido Zarrella, Bruce Torres Fischer, Larry Kimura, Oiwi Parker Jones

Abstract: In this paper we address the challenge of improving Automatic Speech Recognition (ASR) for a low-resource language, Hawaiian, by incorporating large amounts of independent text data into an ASR foundation model, Whisper. To do this, we train an external language model (LM) on ~1.5M words of Hawaiian text. We then use the LM to rescore Whisper and compute word error rates (WERs) on a manually curat… ▽ More In this paper we address the challenge of improving Automatic Speech Recognition (ASR) for a low-resource language, Hawaiian, by incorporating large amounts of independent text data into an ASR foundation model, Whisper. To do this, we train an external language model (LM) on ~1.5M words of Hawaiian text. We then use the LM to rescore Whisper and compute word error rates (WERs) on a manually curated test set of labeled Hawaiian data. As a baseline, we use Whisper without an external LM. Experimental results reveal a small but significant improvement in WER when ASR outputs are rescored with a Hawaiian LM. The results support leveraging all available data in the development of ASR systems for underrepresented languages. △ Less

Submitted 3 April, 2024; originally announced April 2024.

Mining Bug Repositories for Multi-Fault Programs

Authors: Dylan Callaghan, Bernd Fischer

Abstract: Datasets such as Defects4J and BugsInPy that contain bugs from real-world software projects are necessary for a realistic evaluation of automated debugging tools. However these datasets largely identify only a single bug in each entry, while real-world software projects (including those used in Defects4J and BugsInPy) typically contain multiple bugs at the same time. We lift this limitation and de… ▽ More Datasets such as Defects4J and BugsInPy that contain bugs from real-world software projects are necessary for a realistic evaluation of automated debugging tools. However these datasets largely identify only a single bug in each entry, while real-world software projects (including those used in Defects4J and BugsInPy) typically contain multiple bugs at the same time. We lift this limitation and describe an extension to these datasets in which multiple bugs are identified in individual entries. We use test case transplantation and fault location translation, in order to expose and locate the bugs, respectively. We thus provide datasets of true multi-fault versions within real-world software projects, which maintain the properties and usability of the original datasets. △ Less

Submitted 10 April, 2024; v1 submitted 28 March, 2024; originally announced March 2024.

Comments: 9 pages, LaTeX; references for dataset projects added

ACM Class: D.2.5

Improving Spectrum-Based Localization of Multiple Faults by Iterative Test Suite Reduction

Authors: Dylan Callaghan, Bernd Fischer

Abstract: Spectrum-based fault localization (SBFL) works well for single-fault programs but its accuracy decays for increasing fault numbers. We present FLITSR (Fault Localization by Iterative Test Suite Reduction), a novel SBFL extension that improves the localization of a given base metric specifically in the presence of multiple faults. FLITSR iteratively selects reduced versions of the test suite that b… ▽ More Spectrum-based fault localization (SBFL) works well for single-fault programs but its accuracy decays for increasing fault numbers. We present FLITSR (Fault Localization by Iterative Test Suite Reduction), a novel SBFL extension that improves the localization of a given base metric specifically in the presence of multiple faults. FLITSR iteratively selects reduced versions of the test suite that better localize the individual faults in the system. This allows it to identify and re-rank faults ranked too low by the base metric because they were masked by other program elements. We evaluated FLITSR over method-level spectra from an existing large synthetic dataset comprising 75000 variants of 15 open-source projects with up to 32 injected faults, as well as method-level and statement-level spectra from a new dataset with 326 true multi-fault versions from the Defects4J benchmark set containing up to 14 real faults. For all three spectrum types we consistently see substantial reductions of the average wasted efforts at different fault levels, of 30%-90% over the best base metric, and generally similarly large increases in precision and recall, albeit with larger variance across the underlying projects. For the method-level real faults, FLITSR also substantially outperforms GRACE, a state-of-the-art learning-based fault localizer. △ Less

Submitted 16 June, 2023; originally announced June 2023.

Paramater Optimization for Manipulator Motion Planning using a Novel Benchmark Set

Authors: Carl Gaebert, Sascha Kaden, Benjamin Fischer, Ulrike Thomas

Abstract: Sampling-based motion planning algorithms have been continuously developed for more than two decades. Apart from mobile robots, they are also widely used in manipulator motion planning. Hence, these methods play a key role in collaborative and shared workspaces. Despite numerous improvements, their performance can highly vary depending on the chosen parameter setting. The optimal parameters depend… ▽ More Sampling-based motion planning algorithms have been continuously developed for more than two decades. Apart from mobile robots, they are also widely used in manipulator motion planning. Hence, these methods play a key role in collaborative and shared workspaces. Despite numerous improvements, their performance can highly vary depending on the chosen parameter setting. The optimal parameters depend on numerous factors such as the start state, the goal state and the complexity of the environment. Practitioners usually choose these values using their experience and tedious trial and error experiments. To address this problem, recent works combine hyperparameter optimization methods with motion planning. They show that tuning the planner's parameters can lead to shorter planning times and lower costs. It is not clear, however, how well such approaches generalize to a diverse set of planning problems that include narrow passages as well as barely cluttered environments. In this work, we analyze optimized planner settings for a large set of diverse planning problems. We then provide insights into the connection between the characteristics of the planning problem and the optimal parameters. As a result, we provide a list of recommended parameters for various use-cases. Our experiments are based on a novel motion planning benchmark for manipulators which we provide at https://mytuc.org/rybj. △ Less

Submitted 28 February, 2023; originally announced February 2023.

Comments: 9 pages

Journal ref: 2023 IEEE International Conference on Robotics and Automation (ICRA), London, United Kingdom, 2023, pp. 9218-9223

Adaptive Neural Network-based OFDM Receivers

Authors: Moritz Benedikt Fischer, Sebastian Dörner, Sebastian Cammerer, Takayuki Shimizu, Hongsheng Lu, Stephan ten Brink

Abstract: We propose and examine the idea of continuously adapting state-of-the-art neural network (NN)-based orthogonal frequency division multiplex (OFDM) receivers to current channel conditions. This online adaptation via retraining is mainly motivated by two reasons: First, receiver design typically focuses on the universal optimal performance for a wide range of possible channel realizations. However,… ▽ More We propose and examine the idea of continuously adapting state-of-the-art neural network (NN)-based orthogonal frequency division multiplex (OFDM) receivers to current channel conditions. This online adaptation via retraining is mainly motivated by two reasons: First, receiver design typically focuses on the universal optimal performance for a wide range of possible channel realizations. However, in actual applications and within short time intervals, only a subset of these channel parameters is likely to occur, as macro parameters, e.g., the maximum channel delay, can assumed to be static. Second, in-the-field alterations like temporal interferences or other conditions out of the originally intended specifications can occur on a practical (real-world) transmission. While conventional (filter-based) systems would require reconfiguration or additional signal processing to cope with these unforeseen conditions, NN-based receivers can learn to mitigate previously unseen effects even after their deployment. For this, we showcase on-the-fly adaption to current channel conditions and temporal alterations solely based on recovered labels from an outer forward error correction (FEC) code without any additional piloting overhead. To underline the flexibility of the proposed adaptive training, we showcase substantial gains for scenarios with static channel macro parameters, for out-of-specification usage and for interference compensation. △ Less

Submitted 21 July, 2022; v1 submitted 25 March, 2022; originally announced March 2022.

Comments: Submitted to SPAWC 2022

Wiener Filter versus Recurrent Neural Network-based 2D-Channel Estimation for V2X Communications

Authors: Moritz Benedikt Fischer, Sebastian Dörner, Sebastian Cammerer, Takayuki Shimizu, Bin Cheng, Hongsheng Lu, Stephan ten Brink

Abstract: We compare the potential of neural network (NN)-based channel estimation with classical linear minimum mean square error (LMMSE)-based estimators, also known as Wiener filtering. For this, we propose a low-complexity recurrent neural network (RNN)-based estimator that allows channel equalization of a sequence of channel observations based on independent time- and frequency-domain long short-term m… ▽ More We compare the potential of neural network (NN)-based channel estimation with classical linear minimum mean square error (LMMSE)-based estimators, also known as Wiener filtering. For this, we propose a low-complexity recurrent neural network (RNN)-based estimator that allows channel equalization of a sequence of channel observations based on independent time- and frequency-domain long short-term memory (LSTM) cells. Motivated by Vehicle-to-Everything (V2X) applications, we simulate time- and frequency-selective channels with orthogonal frequency division multiplex (OFDM) and extend our channel models in such a way that a continuous degradation from line-of-sight (LoS) to non-line-of-sight (NLoS) conditions can be emulated. It turns out that the NN-based system cannot just compete with the LMMSE equalizer, but it also can be trained w.r.t. resilience against system parameter mismatch. We thereby showcase the conceptual simplicity of such a data-driven system design, as this not only enables more robustness against, e.g., signal-to-noise-ratio (SNR) or Doppler spread estimation mismatches, but also allows to use the same equalizer over a wider range of input parameters without the need of re-building (or re-estimating) the filter coefficients. Particular attention has been paid to ensure compatibility with the existing IEEE 802.11p piloting scheme for V2X communications. Finally, feeding the payload data symbols as additional equalizer input unleashes further performance gains. We show significant gains over the conventional LMMSE equalization for highly dynamic channel conditions if such a data-augmented equalization scheme is used. △ Less

Submitted 21 May, 2021; v1 submitted 5 February, 2021; originally announced February 2021.

Comments: Accepted at 32nd IEEE Intelligent Vehicles Symposium

SMT-Based Refutation of Spurious Bug Reports in the Clang Static Analyzer

Authors: Mikhail R. Gadelha, Enrico Steffinlongo, Lucas C. Cordeiro, Bernd Fischer, Denis A. Nicole

Abstract: We describe and evaluate a bug refutation extension for the Clang Static Analyzer (CSA) that addresses the limitations of the existing built-in constraint solver. In particular, we complement CSA's existing heuristics that remove spurious bug reports. We encode the path constraints produced by CSA as Satisfiability Modulo Theories (SMT) problems, use SMT solvers to precisely check them for satisfi… ▽ More We describe and evaluate a bug refutation extension for the Clang Static Analyzer (CSA) that addresses the limitations of the existing built-in constraint solver. In particular, we complement CSA's existing heuristics that remove spurious bug reports. We encode the path constraints produced by CSA as Satisfiability Modulo Theories (SMT) problems, use SMT solvers to precisely check them for satisfiability, and remove bug reports whose associated path constraints are unsatisfiable. Our refutation extension refutes spurious bug reports in 8 out of 12 widely used open-source applications; on average, it refutes ca. 7% of all bug reports, and never refutes any true bug report. It incurs only negligible performance overheads, and on average adds 1.2% to the runtime of the full Clang/LLVM toolchain. A demonstration is available at {\tt https://www.youtube.com/watch?v=ylW5iRYNsGA}. △ Less

Submitted 30 November, 2018; v1 submitted 29 October, 2018; originally announced October 2018.

Comments: 4 pages

Design and Execution of make-like, distributed Analyses based on Spotify's Pipelining Package Luigi

Authors: Marcel Rieger, Martin Erdmann, Benjamin Fischer, Robert Fischer

Abstract: In high-energy particle physics, workflow management systems are primarily used as tailored solutions in dedicated areas such as Monte Carlo production. However, physicists performing data analyses are usually required to steer their individual workflows manually which is time-consuming and often leads to undocumented relations between particular workloads. We present a generic analysis design pat… ▽ More In high-energy particle physics, workflow management systems are primarily used as tailored solutions in dedicated areas such as Monte Carlo production. However, physicists performing data analyses are usually required to steer their individual workflows manually which is time-consuming and often leads to undocumented relations between particular workloads. We present a generic analysis design pattern that copes with the sophisticated demands of end-to-end HEP analyses and provides a make-like execution system. It is based on the open-source pipelining package Luigi which was developed at Spotify and enables the definition of arbitrary workloads, so-called Tasks, and the dependencies between them in a lightweight and scalable structure. Further features are multi-user support, automated dependency resolution and error handling, central scheduling, and status visualization in the web. In addition to already built-in features for remote jobs and file systems like Hadoop and HDFS, we added support for WLCG infrastructure such as LSF and CREAM job submission, as well as remote file access through the Grid File Access Library. Furthermore, we implemented automated resubmission functionality, software sandboxing, and a command line interface with auto-completion for a convenient working environment. For the implementation of a $t\bar{t}H$ cross section measurement, we created a generic Python interface that provides programmatic access to all external information such as datasets, physics processes, statistical models, and additional files and values. In summary, the setup enables the execution of the entire analysis in a parallelized and distributed fashion with a single command. △ Less

Submitted 3 June, 2017; originally announced June 2017.

Verifying Embedded C Software with Timing Constraints using an Untimed Model Checker

Authors: Raimundo Barreto, Lucas Cordeiro, Bernd Fischer

Abstract: Embedded systems are everywhere, from home appliances to critical systems such as medical devices. They usually have associated timing constraints that need to be verified for the implementation. Here, we use an untimed bounded model checker to verify timing properties of embedded C programs. We propose an approach to specify discrete time timing constraints using code annotations. The annotated c… ▽ More Embedded systems are everywhere, from home appliances to critical systems such as medical devices. They usually have associated timing constraints that need to be verified for the implementation. Here, we use an untimed bounded model checker to verify timing properties of embedded C programs. We propose an approach to specify discrete time timing constraints using code annotations. The annotated code is then automatically translated to code that manipulates auxiliary timer variables and is thus suitable as input to conventional, untimed software model checker such as ESBMC. Thus, we can check timing constraints in the same way and at the same time as untimed system requirements, and even allow for interaction between them. We applied the proposed method in a case study, and verified timing constraints of a pulse oximeter, a noninvasive medical device that measures the oxygen saturation of arterial blood. △ Less

Submitted 12 June, 2011; originally announced June 2011.

Comments: 16 pages

Model-Based Development of Distributed Embedded Systems by the Example of the Scicos/SynDEx Framework

Authors: Bernhard Fischer

Abstract: The embedded systems engineering industry faces increasing demands for more functionality, rapidly evolving components, and shrinking schedules. Abilities to quickly adapt to changes, develop products with safe design, minimize project costs, and deliver timely are needed. Model-based development (MBD) follows a separation of concerns by abstracting systems with an appropriate intensity. MBD promi… ▽ More The embedded systems engineering industry faces increasing demands for more functionality, rapidly evolving components, and shrinking schedules. Abilities to quickly adapt to changes, develop products with safe design, minimize project costs, and deliver timely are needed. Model-based development (MBD) follows a separation of concerns by abstracting systems with an appropriate intensity. MBD promises higher comprehension by modeling on several abstraction-levels, formal verification, and automated code generation. This thesis demonstrates MBD with the Scicos/SynDEx framework on a distributed embedded system. Scicos is a modeling and simulation environment for hybrid systems. SynDEx is a rapid prototy** integrated development environment for distributed systems. Performed examples implement well-known control algorithms on a target system containing several networked microcontrollers, sensors, and actuators. The addressed research question tackles the feasibility of MBD for medium-sized embedded systems. In the case of single-processor applications experiments show that the comforts of tool-provided simulation, verification, and code-generation have to be weighed against an additional memory consumption in dynamic and static memory compared to a hand-written approach. Establishing a near-seamless modeling-framework with Scicos/SynDEx is expensive. An increased development effort indicates a high price for develo** single applications, but might pay off for product families. A further drawback was that the distributed code generated with SynDEx could not be adapted to microcontrollers without a significant alteration of the scheduling tables. The Scicos/SynDEx framework forms a valuable tool set that, however, still needs many improvements. Therefore, its usage is only recommended for experimental purposes. △ Less

Submitted 19 October, 2010; originally announced October 2010.

Comments: 146 pages, Master's Thesis

ACM Class: C.0; C.1.m; D.2.2; D.2.11; D.4.7; D.4.8

Bounded Model Checking of Multi-threaded Software using SMT solvers

Authors: Lucas Cordeiro, Bernd Fischer

Abstract: The transition from single-core to multi-core processors has made multi-threaded software an important subject in computer aided verification. Here, we describe and evaluate an extension of the ESBMC model checker to support the verification of multi-threaded software with shared variables and locks using bounded model checking (BMC) based on Satisfiability Modulo Theories (SMT). We describe three… ▽ More The transition from single-core to multi-core processors has made multi-threaded software an important subject in computer aided verification. Here, we describe and evaluate an extension of the ESBMC model checker to support the verification of multi-threaded software with shared variables and locks using bounded model checking (BMC) based on Satisfiability Modulo Theories (SMT). We describe three approaches to model check multi-threaded software and our modelling of the synchronization primitives of the Pthread library. In the lazy approach, we generate all possible interleavings and call the BMC procedure on each of them individually, until we either find a bug, or have systematically explored all interleavings. In the schedule recording approach, we encode all possible interleavings into one single formula and then exploit the high speed of the SMT solvers. In the underapproximation-widening approach, we reduce the state space by abstracting the number of state variables and interleavings from the proofs of unsatisfiability generated by the SMT solvers. In all three approaches, we use partial-order reduction (POR) techniques to reduce the number of interleavings explored. Experiments show that our approaches can analyze larger problems and substantially reduce the verification time compared to state-of-the-art techniques that combine classic POR methods with symbolic algorithms and others that implement the Counter-Example Guided Abstraction Refinement technique. △ Less

Submitted 19 March, 2010; originally announced March 2010.

Continuous Verification of Large Embedded Software using SMT-Based Bounded Model Checking

Authors: Lucas Cordeiro, Bernd Fischer, Joao Marques-Silva

Abstract: The complexity of software in embedded systems has increased significantly over the last years so that software verification now plays an important role in ensuring the overall product quality. In this context, SAT-based bounded model checking has been successfully applied to discover subtle errors, but for larger applications, it often suffers from the state space explosion problem. This paper… ▽ More The complexity of software in embedded systems has increased significantly over the last years so that software verification now plays an important role in ensuring the overall product quality. In this context, SAT-based bounded model checking has been successfully applied to discover subtle errors, but for larger applications, it often suffers from the state space explosion problem. This paper describes a new approach called continuous verification to detect design errors as quickly as possible by looking at the Software Configuration Management (SCM) system and by combining dynamic and static verification to reduce the state space to be explored. We also give a set of encodings that provide accurate support for program verification and use different background theories in order to improve scalability and precision in a completely automatic way. A case study from the telecommunications domain shows that the proposed approach improves the error-detection capability and reduces the overall verification time by up to 50%. △ Less

Submitted 19 November, 2009; originally announced November 2009.

Industrial-Strength Formally Certified SAT Solving

Authors: Ashish Darbari, Bernd Fischer, Joao Marques-Silva

Abstract: Boolean Satisfiability (SAT) solvers are now routinely used in the verification of large industrial problems. However, their application in safety-critical domains such as the railways, avionics, and automotive industries requires some form of assurance for the results, as the solvers can (and sometimes do) have bugs. Unfortunately, the complexity of modern, highly optimized SAT solvers renders… ▽ More Boolean Satisfiability (SAT) solvers are now routinely used in the verification of large industrial problems. However, their application in safety-critical domains such as the railways, avionics, and automotive industries requires some form of assurance for the results, as the solvers can (and sometimes do) have bugs. Unfortunately, the complexity of modern, highly optimized SAT solvers renders impractical the development of direct formal proofs of their correctness. This paper presents an alternative approach where an untrusted, industrial-strength, SAT solver is plugged into a trusted, formally certified, SAT proof checker to provide industrial-strength certified SAT solving. The key novelties and characteristics of our approach are (i) that the checker is automatically extracted from the formal development, (ii), that the combined system can be used as a standalone executable program independent of any supporting theorem prover, and (iii) that the checker certifies any SAT solver respecting the agreed format for satisfiability and unsatisfiability claims. The core of the system is a certified checker for unsatisfiability claims that is formally designed and verified in Coq. We present its formal design and outline the correctness proofs. The actual standalone checker is automatically extracted from the the Coq development. An evaluation of the certified checker on a representative set of industrial benchmarks from the SAT Race Competition shows that, albeit it is slower than uncertified SAT checkers, it is significantly faster than certified checkers implemented on top of an interactive theorem prover. △ Less

Submitted 17 December, 2009; v1 submitted 9 November, 2009; originally announced November 2009.

SMT-Based Bounded Model Checking for Embedded ANSI-C Software

Authors: Lucas Cordeiro, Bernd Fischer, Joao Marques-Silva

Abstract: Propositional bounded model checking has been applied successfully to verify embedded software but is limited by the increasing propositional formula size and the loss of structure during the translation. These limitations can be reduced by encoding word-level information in theories richer than propositional logic and using SMT solvers for the generated verification conditions. Here, we investi… ▽ More Propositional bounded model checking has been applied successfully to verify embedded software but is limited by the increasing propositional formula size and the loss of structure during the translation. These limitations can be reduced by encoding word-level information in theories richer than propositional logic and using SMT solvers for the generated verification conditions. Here, we investigate the application of different SMT solvers to the verification of embedded software written in ANSI-C. We have extended the encodings from previous SMT-based bounded model checkers to provide more accurate support for finite variables, bit-vector operations, arrays, structures, unions and pointers. We have integrated the CVC3, Boolector, and Z3 solvers with the CBMC front-end and evaluated them using both standard software model checking benchmarks and typical embedded applications from telecommunications, control systems and medical devices. The experiments show that our approach can analyze larger problems and substantially reduce the verification time. △ Less

Submitted 13 July, 2009; v1 submitted 12 July, 2009; originally announced July 2009.

Comments: 12 pages

Numerical removal of water-vapor effects from THz-TDS measurements

Authors: Withawat Withayachumnankul, Bernd M. Fischer, Samuel P. Mickan, Derek Abbott

Abstract: One source of disturbance in a pulsed T-ray signal is attributed to ambient water vapor. Water molecules in the gas phase selectively absorb T-rays at discrete frequencies corresponding to their molecular rotational transitions. This results in prominent resonances spread over the T-ray spectrum, and in the time domain the T-ray signal is observed as fluctuations after the main pulse. These effe… ▽ More One source of disturbance in a pulsed T-ray signal is attributed to ambient water vapor. Water molecules in the gas phase selectively absorb T-rays at discrete frequencies corresponding to their molecular rotational transitions. This results in prominent resonances spread over the T-ray spectrum, and in the time domain the T-ray signal is observed as fluctuations after the main pulse. These effects are generally undesired, since they may mask critical spectroscopic data. So, ambient water vapor is commonly removed from the T-ray path by using a closed chamber during the measurement. Yet, in some applications a closed chamber is not applicable. This situation, therefore, motivates the need for another method to reduce these unwanted artifacts. This paper presents a study on a computational means to address the problem. Initially, a complex frequency response of water vapor is modeled from a spectroscopic catalog. Using a deconvolution technique, together with fine tuning of the strength of each resonance, parts of the water-vapor response are removed from a measured T-ray signal, with minimal signal distortion. △ Less

Submitted 18 October, 2007; originally announced October 2007.

Journal ref: Proceedings of the Royal Society A: Mathematical, Physical & Engineering Sciences, vol. 464, no. 2097, pp 2435-2456, 2008