Repository for Publications and Research Data
News from the ETH Library
Recently Added
Huber, Sebastian (2026)
Soom, Florian; Guglielmi, Yves; Cook, Paul; et al. (2026)
This report documents 11 tests carried out with the SIMFIP probe in borehole BFE_A_05 at the BedrettoLab between 30 November and 9 December 2022. The tests aim to establish a stress profile across the MC fault zone. Test intervals were selected from borehole logs and cores to represent both intact rock and pre-existing fractures. Three intervals are located above the fault zone, seven below it, and one cross-hole test was carried out within it. Each test followed a modified HTPF protocol of pressure step cycles below the expected fracturing or fracture stimulation pressure, followed by constant flow rate cycles to initiate new fractures or stimulate pre-existing ones. Three-dimensional displacements of the borehole wall were recorded at 40 Hz throughout each test.
All tests were completed successfully. For each test, the report presents:
- the pressure and flow rate records;
- the picked incremental displacement vectors;
- the activation vector associated with non-elastic fracture slip and opening;
- the activation vector’s normal and tangential components on the most likely activated fracture plane identified from acoustic televiewer logs.
Fusion: A Fold and Unfold Annotation Synthesis Tool for Viper-Based Verification
Item type: Conference Paper
Lee, Joonghoon; Klose, Nicolas; Lee, Seokhyun; et al. (2026)
Viper is a verification infrastructure for permission-based reasoning and serves as a common back-end for verifiers targeting multiple programming languages. In Viper, predicates package heap resources into reusable abstractions. To prevent SMT solvers from unfolding recursive predicates indefinitely, Viper treats predicates isorecursively: a predicate instance is not automatically interchangeable with the resources described by its body. Consequently, users must provide explicit fold/unfold annotations to transition between abstraction levels.
To address this issue, we present Fusion, a Viper-based tool that synthesizes missing fold/unfold annotations, built around a novel graph-based synthesis method. Given a verification failure due to a missing resource, Fusion constructs a predicate dependency graph from Viper predicate definitions and finds potential ways to obtain the missing resource from available resources, thereby formulating annotation synthesis as a pathfinding problem over the graph. It uses the resulting paths to synthesize candidate sequences of fold/unfold annotations that potentially provide the missing resource, and uses the verifier to validate the annotations. Our evaluation on a large real-world verification project shows that Fusion successfully synthesizes annotations for 93 of 149 benchmark functions (62.4%) within a 20-minute per-function budget, demonstrating its potential to reduce the annotation burden in practical verification workflows.
Circular Dichroism (CD) Spectroscopy Analysis Of Chimeric Hepatitis B Virus Core Antigen (HBc) Virus-like Particles Displaying SARS-CoV-2 Spike Protein Epitopes
Item type: Dataset
Qureshi, Bilal M. (2026)
Mass-spectrometric Identification Of Chimeric Hepatitis B Virus Core Antigen (HBc) Virus-like Particles Displaying SARS-CoV-2 Spike Protein Epitopes
Item type: Dataset
Qureshi, Bilal M. (2026)