-
Article
On compiling Boolean circuits optimized for secure multi-party computation
Secure multi-party computation (MPC) allows two or more distrusting parties to jointly evaluate a function over private inputs. For a long time considered to be a purely theoretical concept, MPC transitioned i...
-
Chapter and Conference Paper
Compiling Low Depth Circuits for Practical Secure Computation
With the rise of practical Secure Multi-party Computation (MPC) protocols, compilers have been developed that create Boolean or Arithmetic circuits for MPC from functionality descriptions in a high-level langu...
-
Chapter and Conference Paper
Error Invariants for Concurrent Traces
Error invariants are assertions that over-approximate the reachable program states at a given position in an error trace while only capturing states that will still lead to failure if execution of the trace is...
-
Chapter and Conference Paper
Facilitating Reuse in Multi-goal Test-Suite Generation for Software Product Lines
Software testing is still the most established and scalable quality-assurance technique in practice. However, generating effective test suites remains computationally expensive, consisting of repetitive reacha...
-
Chapter and Conference Paper
CBMC-GC: An ANSI C Compiler for Secure Two-Party Computations
Secure two-party computation (STC) is a computer security paradigm where two parties can jointly evaluate a program with sensitive input data, provided in parts from both parties. By the security guarantees of...
-
Chapter and Conference Paper
Information Reuse for Multi-goal Reachability Analyses
It is known that model checkers can generate test inputs as witnesses for reachability specifications (or, equivalently, as counterexamples for safety properties). While this use of model checkers for testing ...
-
Chapter and Conference Paper
Solving Constraints for Generational Search
Concolic testing is an automated software testing method that combines concrete and symbolic execution to achieve high code coverage and expose bugs in the program under test. During an execution of the progra...
-
Article
Application and survival curve of total hip arthroplasties: a systematic comparative analysis using worldwide hip arthroplasty registers
The aim of the study was to compare primary total hip arthroplasty (THA) implantations between different countries in terms of THA number per inhabitant, age, and procedure type and to compare the survival cur...
-
Chapter and Conference Paper
Vinter: A Vampire-Based Tool for Interpolation
This paper describes the Vinter tool for extracting interpolants from proofs and minimising such interpolants using various measures. Vinter takes an input problem written in either SMT-LIB or TPTP syntax, gen...
-
Chapter and Conference Paper
Proving Reachability Using FShell
FShell is an automated white-box test-input generator for C programs, computing test data with respect to user-specified code coverage criteria. The pillars of FShell are the declarative specific...
-
Chapter and Conference Paper
Bounded-Interference Sequentialization for Testing Concurrent Programs
Testing concurrent programs is a challenging problem: (1) the tester has to come up with a set of input values that may trigger a bug, and (2) even with a bug-triggering input value, there may be a large number o...
-
Article
Open AccessInfraglenoidal scapular notching in reverse total shoulder replacement: a prospective series of 60 cases and systematic review of the literature
The impact of infraglenoidal scapular notching in reversed total shoulder arthroplasty (RTSA) is still controversially discussed. Our goal was to evaluate its potential influence on subjective shoulder stabili...
-
Chapter and Conference Paper
An Introduction to Test Specification in FQL
In a recent series of papers, we introduced a new framework for white-box testing which aims at a separation of concerns between test specifications and test generation engines. We believe that establishing a ...
-
Chapter and Conference Paper
Seamless Testing for Models and Code
This paper describes an approach to model-based testing where a test suite is generated from a model and automatically concretized to drive an implementation. Motivated by an industrial project involving DO-17...
-
Chapter
Do Pharmaceuticals in the Environment Present an Investment Risk?
The Sarasin Group is represented in 19 locations worldwide across Europe, the Middle East and Asia. By June 2009 it managed total client assets of CHF 80 billion and employed over 1,500 staff. Its majority sha...
-
Chapter and Conference Paper
Timely Time Estimates
Estimations of execution time are essential for design and development of safety critical embedded real-time systems, such as avionics, automotive and aerospace systems. In such systems, execution time is part...
-
Chapter and Conference Paper
Query-Driven Program Testing
We present a new approach to program testing which enables the programmer to specify test suites in terms of a versatile query language. Our query language subsumes standard coverage criteria ranging from simp...
-
Chapter and Conference Paper
FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement
Although the principal analogy between counterexample generation and white box testing has been repeatedly addressed, the usage patterns and performance requirements for software testing are quite different fr...
-
Chapter and Conference Paper
Using Verification Technology to Specify and Detect Malware
Computer viruses and worms are major threats for our computer infrastructure, and thus, for economy and society at large. Recent work has demonstrated that a model checking based approach to malware detection ...
