A Set-Based Context Model for Program Analysis
Abstract elided by the publisher.
26,098 papers · page 314 of 1,305
Formal Verification of Atomicity Requirements for Smart Contracts
Abstract elided by the publisher.
A New Refinement Type System for Automated $\nu \text {HFL}_\mathbb {Z}$ Validity Checking
Abstract elided by the publisher.
Neural Networks, Secure by Construction - An Exploration of Refinement Types
Abstract elided by the publisher.
Relational Synthesis for Pattern Matching
Abstract elided by the publisher.
Automatically Generating Descriptive Texts in Logging Statements: How Far Are We?
Abstract elided by the publisher.
Syntactically Restricting Bounded Polymorphism for Decidable Subtyping
Abstract elided by the publisher.
Parameterized Synthesis with Safety Properties
Parameterized synthesis offers a solution to the problem of constructing correct and verified controllers for parameterized systems. Such systems occur naturally in practice (e.g., in the form of distributed protocols where the amount of processes is often unknown at design time …
Stack-Driven Program Generation of WebAssembly
Abstract elided by the publisher.
P3: A Profiler Suite for Parallel Applications on the Java Virtual Machine
Abstract elided by the publisher.
Certified Semantics for Relational Programming
We present a formal study of semantics for relational programming language miniKanren. First, we formulate denotational semantics which corresponds to the minimal Herbrand model for definite logic programs. Second, we present operational semantics which models the distinctive fea…
REFINITY to Model and Prove Program Transformation Rules
Abstract elided by the publisher.
A Counterexample-Guided Debugger for Non-recursive Datalog
Abstract elided by the publisher.
Algebraic and Coalgebraic Perspectives on Interaction Laws
Abstract elided by the publisher.
Reachability Analysis Using Message Passing over Tree Decompositions
In this paper, we study efficient approaches to reachability analysis for discrete-time nonlinear dynamical systems when the dependencies among the variables of the system have low treewidth. Reachability analysis over nonlinear dynamical systems asks if a given set of target sta…
MetaVal: Witness Validation via Verification
Witness validation is an important technique to increase trust in verification results, by making descriptions of error paths (violation witnesses) and important parts of the correctness proof (correctness witnesses) available in an exchangeable format. This way, the verification…
End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract
We report our experience in the formal verification of the deposit smart contract, whose correctness is critical for the security of Ethereum 2.0, a new Proof-of-Stake protocol for the Ethereum blockchain. The deposit contract implements an incremental Merkle tree algorithm whose…
SeQuaiA: A Scalable Tool for Semi-Quantitative Analysis of Chemical Reaction Networks
Chemical reaction networks (CRNs) play a fundamental role in analysis and design of biochemical systems. They induce continuous-time stochastic systems, whose analysis is a computationally intensive task. We present a tool that implements the recently proposed semi-quantitative a…
A Novel Approach for Solving the BMI Problem in Barrier Certificates Generation
Barrier certificates generation is widely used in verifying safety properties of hybrid systems because of the relatively low computational complexity it costs. Under sum of squares (SOS) relaxation, the problem of barrier certificate generation is equivalent to that of solving a…
Synthesis of Super-Optimized Smart Contracts Using Max-SMT
With the advent of smart contracts that execute on the blockchain ecosystem, a new mode of reasoning is required for developers that must pay meticulous attention to the gas spent by their smart contracts, as well as for optimization tools that must be capable of effectively redu…