arXiv subjects

Thomas Lemberger

Publications and source records attributed to Thomas Lemberger.

3 recordsLinked to original sources

arXiv2024

Software Verification with CPAchecker 3.0: Tutorial and User Guide (Extended Version)

This tutorial provides an introduction to CPAchecker for users. CPAchecker is a flexible and configurable framework for software verification and testing. The framework provides many abstract domains, such as BDDs, explicit values, intervals, memory graphs, and predicates, and many program-analysis and model-checking algorithms, such as abstract interpretation, bounded model checking, Impact, interpolation-based model checking, k -induction, PDR, predicate abstraction, and symbolic execution. This tutorial presents basic use cases for CPAchecker in formal software verification, focusing on its main verification techniques with their strengths and weaknesses. It also shows further use cases of CPAchecker for test-case generation and witness-based result validation. The envisioned readers are assumed to possess a background in automatic formal verification and program analysis, but prior knowledge of CPAchecker is not required. This tutorial and user guide is based on CPAchecker in version 3.0. This user guide's latest version and other documentation are available at https://cpachecker.sosy-lab.org/doc.php.

cs.SE↗

arXiv2023

Integrating curation into scientific publishing to train AI models

High throughput extraction and structured labeling of data from academic articles is critical to enable downstream machine learning applications and secondary analyses. We have embedded multimodal data curation into the academic publishing process to annotate segmented figure panels and captions. Natural language processing (NLP) was combined with human-in-the-loop feedback from the original authors to increase annotation accuracy. Annotation included eight classes of bioentities (small molecules, gene products, subcellular components, cell lines, cell types, tissues, organisms, and diseases) plus additional classes delineating the entities' roles in experiment designs and methodologies. The resultant dataset, SourceData-NLP, contains more than 620,000 annotated biomedical entities, curated from 18,689 figures in 3,223 articles in molecular and cell biology. We evaluate the utility of the dataset to train AI models using named-entity recognition, segmentation of figure captions into their constituent panels, and a novel context-dependent semantic task assessing whether an entity is a controlled intervention target or a measurement object. We also illustrate the use of our dataset in performing a multi-modal task for segmenting figures into panel images and their corresponding captions.

cs.CL↗

arXiv2021

Towards a Benchmark Set for Program Repair Based on Partial Fixes

Software bugs significantly contribute to software cost and increase the risk of system malfunctioning. In recent years, many automated program-repair approaches have been proposed to automatically fix undesired program behavior. Despite of their great success, specific problems such as fixing bugs with partial fixes still remain unresolved. A partial fix to a known software issue is a programmer's failed attempt to fix the issue the first time. Even though it fails, this fix attempt still conveys important information such as the suspicious software region and the bug type. In this work we do not propose an approach for program repair with partial fixes, but instead answer a preliminary question: Do partial fixes occur often enough, in general, to be relevant for the research area of automated program repair? We crawled 1500 open-source C repositories on GitHub for partial fixes. The result is a benchmark set of 2204 benchmark tasks for automated program repair based on partial fixes. The benchmark set is available open source and open to further contributions and improvement.

cs.SE↗