SearcharxivSearch

arXiv subjects

Torben Amtoft

Publications and source records attributed to Torben Amtoft.

5 recordsLinked to original sources

A Fast Algorithm for Finding Minimum Weight Cycles in Mining Cyclic Graph Topologies

Cyclic structures are fundamental topological features in graphs, playing critical roles in network robustness, information flow, community structure, and various dynamic processes. Algorithmic tools that can efficiently probe and analyze these cyclic topologies are increasingly vital for tasks in graph mining, network optimization, bioinformatics, and social network analysis. A core primitive for quantitative analysis of cycles is finding the Minimum Weight Cycle (MWC), representing the shortest cyclic path in a weighted graph. However, computing the MWC efficiently remains a challenge, particularly compared to shortest path computations. This paper introduces a novel deterministic algorithm for finding the MWC in general weighted graphs. Our approach adapts the structure of Dijkstra's algorithm by introducing and minimizing a \textit{composite distance} metric, effectively translating the global cycle search into an iterative node-centric optimization. We provide a rigorous proof of correctness based on loop invariants. We detail two mechanisms for accelerating the search: a provable node discarding technique based on intermediate results, and a highly effective graph pruning heuristic. This heuristic dynamically restricts the search to relevant subgraphs, leveraging the principle of locality often present in complex networks to achieve significant empirical speedups, while periodic resets ensure global optimality is maintained. The efficiency of the proposed MWC algorithm enables its use as a core component in more complex analyses focused on cyclic properties. We illustrate this through a detailed application case study: accelerating the computation of the Loop Modulus, a measure of cycle richness used in advanced network characterization. Our algorithm dramatically reduces the runtime of the iterative constraint-finding bottleneck in this computation.

cs.DS

A Fixed Point Iteration Technique for Proving Correctness of Slicing for Probabilistic Programs

When proving the correctness of a method for slicing probabilistic programs, it was previously discovered by the authors that for a fixed point iteration to work one needs a non-standard starting point for the iteration. This paper presents and explores this technique in a general setting; it states the lemmas that must be established to use the technique to prove the correctness of a program transformation, and sketches how to apply the technique to slicing of probabilistic programs.

cs.PL

SeMA: Extending and Analyzing Storyboards to Develop Secure Android Apps

Mobile apps provide various critical services, such as banking, communication, and healthcare. To this end, they have access to our personal information and have the ability to perform actions on our behalf. Hence, securing mobile apps is crucial to ensuring the privacy and safety of its users. Recent research efforts have focused on developing solutions to secure mobile ecosystems (i.e., app platforms, apps, and app stores), specifically in the context of detecting vulnerabilities in Android apps. Despite this attention, known vulnerabilities are often found in mobile apps, which can be exploited by malicious apps to harm the user. Further, fixing vulnerabilities after developing an app has downsides in terms of time, resources, user inconvenience, and information loss. In an attempt to address this concern, we have developed SeMA, a mobile app development methodology that builds on existing mobile app design artifacts such as storyboards. With SeMA, security is a first-class citizen in an app's design -- app designers and developers can collaborate to specify and reason about the security properties of an app at an abstract level without being distracted by implementation level details. Our realization of SeMA using Android Studio tooling demonstrates the methodology is complementary to existing design and development practices. An evaluation of the effectiveness of SeMA shows the methodology can detect and help prevent 49 vulnerabilities known to occur in Android apps. Further, a usability study of the methodology involving ten real-world developers shows the methodology is likely to reduce the development time and help developers uncover and prevent known vulnerabilities while designing apps.

cs.SE

A Theory of Slicing for Probabilistic Control-Flow Graphs

We present a theory for slicing probabilistic imperative programs -- containing random assignments, and ``observe'' statements (for conditioning) -- represented as probabilistic control-flow graphs (pCFGs) whose nodes modify probability distributions. We show that such a representation allows direct adaptation of standard machinery such as data and control dependence, postdominators, relevant variables, etc to the probabilistic setting. We separate the specification of slicing from its implementation: first we develop syntactic conditions that a slice must satisfy; next we prove that any such slice is semantically correct; finally we give an algorithm to compute the least slice. To generate smaller slices, we may in addition take advantage of knowledge that certain loops will terminate (almost) always. A key feature of our syntactic conditions is that they involve two disjoint slices such that the variables of one slice are probabilistically independent of the variables of the other. This leads directly to a proof of correctness of probabilistic slicing. In a companion article we show adequacy of the semantics of pCFGs with respect to the standard semantics of structured probabilistic programs.

cs.PL

A Semantics for Probabilistic Control-Flow Graphs

This article develops a novel operational semantics for probabilistic control-flow graphs (pCFGs) of probabilistic imperative programs with random assignment and "observe" (or conditioning) statements. The semantics transforms probability distributions (on stores) as control moves from one node to another in pCFGs. We relate this semantics to a standard, expectation-transforming, denotational semantics of structured probabilistic imperative programs, by translating structured programs into (unstructured) pCFGs, and proving adequacy of the translation. This shows that the operational semantics can be used without loss of information, and is faithful to the "intended" semantics and hence can be used to reason about, for example, the correctness of transformations (as we do in a companion article).

cs.PL