More Like this

1. Minimally Comparing Relational Abstract Domains

   https://doi.org/10.1007/978-3-031-45332-8_8  

   Ballou, Kenny; Sherman, Elena (October 2023, Automated Technology for Verification and Analysis)

   Andre, Etienne; Sun, Jun (Ed.)

   Value-based static analysis techniques express computed program invariants as logical formula over program variables. Researchers and practitioners use these invariants to aid in software engineering and verification tasks. When selecting abstract domains, practitioners weigh the cost of a domain against its expressiveness. However, an abstract domain's expressiveness tends to be stated in absolute terms; either mathematically via the sub-polyhedra the domain is capable of describing, empirically using a set of known properties to verify, or empirically via logical entailment using the entire invariant of the domain at each program point. Due to carry-over effects, however, the last technique can be problematic because it tends to provide simplistic and imprecise comparisons 

   more » « less
2. Strong valid inequalities for a class of concave submodular minimization problems under cardinality constraints

   https://doi.org/10.1007/s10107-022-01921-5  

   Yu, Qimeng; Küçükyavuz, Simge (January 2023, Mathematical Programming)

   We study the polyhedral convex hull structure of a mixed-integer set which arises in a class of cardinality-constrained concave submodular minimization problems. This class of problems has an objective function in the form of $f(a^Tx)$, where f is a univariate concave function, a is a non-negative vector, and x is a binary vector of appropriate dimension. Such minimization problems frequently appear in applications that involve risk-aversion or economies of scale. We propose three classes of strong valid linear inequalities for this convex hull and specify their facet conditions when a has two distinct values. We show how to use these inequalities to obtain valid inequalities for general a that contains multiple values. We further provide a complete linear convex hull description for this mixed-integer set when a contains two distinct values and the cardinality constraint upper bound is two. Our computational experiments on the mean-risk optimization problem demonstrate the effectiveness of the proposed inequalities in a branch-and-cut framework. 

   more » « less
3. On Log Analysis and Stack Trace Use to Improve Program Slicing

   https://doi.org/10.1007/978-981-33-6385-4_25  

   Bushong, Vincent; Sanders, Russell; Curtis, Jacob; Du, Mark; Cerny, Tomas; Frajtak, Karel; Tisnovsky, Pavel; Shin, Dongwan (April 2021, Information Science and Applications. Lecture Notes in Electrical Engineering)

   null; null; null (Ed.)

   Program slicing is a common technique to help reconstruct the path of execution a program has taken. It is beneficial for assisting developers in debugging their programs, but its usefulness depends on the slice accuracy that can be achieved, which is limited by the sources of information used in building the slice. In this paper, we demonstrate that two sources of information, namely program logs, and stack traces, previously used in isolation to build program slices, can be combined to build a program slicer capable of handling more scenarios than either method individually. We also demonstrate a sample application of our proposed slicing approach by showing how our slicer can deduce integer inputs that will recreate the detected error’s execution path. 

   more » « less
4. xJsnark: A Framework for Efficient Verifiable Computation

   Kosba, A.; Papamanthou, C.; Shi, E. (January 2018, IEEE Symposium on Security and Privacy)

   Many cloud and cryptocurrency applications rely on verifying the integrity of outsourced computations, in which a verifier can efficiently verify the correctness of a computation made by an untrusted prover. State-of-the-art protocols for verifiable computation require that the computation task be expressed as arithmetic circuits, and the number of multiplication gates in the circuit is the primary metric that determines performance. At the present, a programmer could rely on two approaches for expressing the computation task, either by composing the circuits directly through low-level development tools; or by expressing the computation in a high-level program and rely on compilers to perform the program-to-circuit transformation. The former approach is difficult to use but on the other hand allows an expert programmer to perform custom optimizations that minimize the resulting circuit. In comparison, the latter approach is much more friendly to non-specialist users, but existing compilers often emit suboptimal circuits. We present xJsnark, a programming framework for verifiable computation that aims to achieve the best of both worlds: offering programmability to non-specialist users, and meanwhile automating the task of circuit size minimization through a combination of techniques. Specifically, we present new circuit-friendly algorithms for frequent operations that achieve constant to asymptotic savings over existing ones; various globally aware optimizations for short- and long- integer arithmetic; as well as circuit minimization techniques that allow us to reduce redundant computation over multiple expressions. We illustrate the savings in different applications, and show the framework's applicability in developing large application circuits, such as ZeroCash, while minimizing the circuit size as in low-level implementations. 

   more » « less
5. Multilayer protection-at-lightpath for reliable slicing with isolation in optical metro-aggregation networks

   https://doi.org/10.1364/JOCN.444522  

   Marotta, A.; Cassioli, D.; Tornatore, M.; Hirota, Y.; Awaji, Y.; Mukherjee, B. (March 2022, Journal of Optical Communications and Networking)

   The high reliability required by many future-generation network services can be enforced by proper resource assignments by means of logical partitions, i.e., network slices, applied in optical metro-aggregation networks. Different strategies can be applied to deploy the virtual network functions (VNFs) composing the slices over physical nodes, while providing different levels of resource isolation (among slices) and protection against failures, based on several available techniques. Considering that, in optical metro-aggregation networks, protection can be ensured at different layers, and the slice protection with traffic grooming calls for evolved multilayer protection approaches. In this paper, we investigate the problem of reliable slicing with protection at the lightpath layer for different levels of slice isolation and different VNF deployment strategies. We model the problem through an integer linear program (ILP), and we devise a heuristic for joint optimization of VNF placement and ligthpath selection. The heuristic maps nodes and links over the physical network in a coordinated manner and provides an effective placement of radio access network functions and the routing and wavelength assignment for the optical layer. The effectiveness of the proposed heuristic is validated by comparison with the optimal solution provided by the ILP. Our illustrative numerical results compare the impact of different levels of isolation, showing that higher levels of network and VNF isolation are characterized by higher costs in terms of optical and computation resources. 

   more » « less