| 1. |
- Aanæs, Henrik, et al.
(författare)
-
Camera Resectioning from a Box
- 2009
-
Ingår i: Lecture Notes in Computer Science. - 0302-9743 .- 1611-3349.
-
Konferensbidrag (refereegranskat)abstract
- In this paper we describe how we can do camera resectioning from a box with unknown dimensions, i.e. determine the camera model, assuming that image pixels are square. This assumption is equivalent to assuming that the camera as an aspect ratio of one and zero skew, and holds for most - if not all - digital cameras. Our proposed method works by first deriving 9 linear constraints on the projective camera matrix from the box, leaving a 3 dimensional subspace in which the projective camera matrix can lye. A single solution in this 3D subspace is then found via a method by Triggs in 1999, which uses the squared pixel assumption to set up a 4th degree polynomial to which the solution is the desired model. This approach is, however, numerically challenging, and we use several means to combat this issue. Lastly the solution is refined in an iterative manner, i.e. using bundle adjustment.
|
|
| 2. |
- Abbasi, Rosa, et al.
(författare)
-
Deductive Verification of Floating-Point Java Programs in KeY
- 2021
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 12652 LNCS, s. 242-261
-
Konferensbidrag (refereegranskat)abstract
- Deductive verification has been successful in verifying interesting properties of real-world programs. One notable gap is the limited support for floating-point reasoning. This is unfortunate, as floating-point arithmetic is particularly unintuitive to reason about due to rounding as well as the presence of the special values infinity and ‘Not a Num-ber’ (NaN). In this paper, we present the first floating-point support in a deductive verification tool for the Java programming language. Our support in the KeY verifier handles arithmetic via floating-point decision procedures inside SMT solvers and transcendental functions via axiomatization. We evaluate this integration on new benchmarks, and show that this approach is powerful enough to prove the absence of floating-point special values—often a prerequisite for further reasoning about numerical computations—as well as certain functional properties for realistic benchmarks.
|
|
| 3. |
- Abd Alrahman, Yehia, 1986, et al.
(författare)
-
A PO Characterisation ofReconfiguration
- 2022
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349.
-
Konferensbidrag (refereegranskat)abstract
- We consider partial order semantics of concurrent systems in which local reconfigurations may have global side effects. That is, local changes happening to an entity may block or unblock events relating to others, namely, events in which the entity does not participate. We show that partial order computations need to capture additional restrictions about event ordering, i.e., restrictions that arise from such reconfigurations. This introduces ambiguity where different partial orders represent exactly the same events with the same participants happening in different orders, thus defeating the purpose of using partial order semantics. To remove this ambiguity, we suggest an extension of partial orders called glued partial orders. We show that glued partial orders capture all possible forced reordering arising from said reconfigurations. Furthermore, we show that computations belonging to different glued partial orders are only different due to non-determinism. We consider channeled transition systems and Petri-nets with inhibiting arcs as examples.
|
|
| 4. |
- Abd Alrahman, Yehia, 1986, et al.
(författare)
-
Model Checking Reconfigurable Interacting Systems
- 2022
-
Ingår i: Lecture Notes in Computer Science book series (LNCS,volume 13703). - Cham : Springer, Cham. - 0302-9743 .- 1611-3349. - 9783031197581
-
Konferensbidrag (refereegranskat)abstract
- Reconfigurable multi-agent systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interactions interfaces by forming collectives, and interact based on mutual interests. Finding ways to design and analyse the behaviour of these systems is a vigorously pursued research goal. We propose a model checker, named R-CHECK (Find the associated toolkit repository here: https://github.com/dsynma/recipe.), to allow reasoning about these systems both from an individual- and a system- level. R-CHECK also permits reasoning about interaction protocols and joint missions. R-CHECK supports a high-level input language with symbolic semantics, and provides a modelling convenience for interaction features such as reconfiguration, coalition formation, and self-organisation.
|
|
| 5. |
- Abd Alrahman, Yehia, 1986, et al.
(författare)
-
Testing for coordination fidelity : Testing for coordination fidelity
- 2019
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349. ; , s. 152-169
-
Bokkapitel (refereegranskat)abstract
- © Springer Nature Switzerland AG 2019. Operation control in modern distributed systems must rely on decentralised coordination among system participants. In particular when the operation control involves critical infrastructures such as power grids, it is vital to ensure correctness properties of such coordination mechanisms. In this paper, we present a verification technique that addresses coordination protocols for power grid operation control. Given a global protocol specification, we show how we can rely on testing semantics for the purpose of ensuring protocol fidelity, i.e., to certify that the interaction among the grid nodes follows the protocol specification.
|
|
| 6. |
- Abdelraheem, Mohamed Ahmed, et al.
(författare)
-
On The Distribution of Linear Biases: Three Instructive Examples
- 2012
-
Ingår i: Lecture Notes in Computer Science : Advances in Cryptology – CRYPTO 2012 32nd Annual Cryptology Conference, Santa Barbara, CA, USA, August 19-23, 2012. Proceedings - Advances in Cryptology – CRYPTO 2012 32nd Annual Cryptology Conference, Santa Barbara, CA, USA, August 19-23, 2012. Proceedings. - Berlin, Heidelberg : Springer Berlin Heidelberg. - 0302-9743 .- 1611-3349. - 9783642320088 - 9783642320095 ; 7417, s. 50-67
-
Konferensbidrag (refereegranskat)abstract
- Despite the fact that we evidently have very good block ciphers at hand today, some fundamental questions on their security are still unsolved. One such fundamental problem is to precisely assess the security of a given block cipher with respect to linear cryptanalysis. In by far most of the cases we have to make (clearly wrong) assumptions, e.g., assume independent round-keys. Besides being unsatisfactory from a scientific perspective, the lack of fundamental understanding might have an impact on the performance of the ciphers we use. As we do not understand the security sufficiently enough, we often tend to embed a security margin -- from an efficiency perspective nothing else than wasted performance. The aim of this paper is to stimulate research on these foundations of block ciphers. We do this by presenting three examples of ciphers that behave differently to what is normally assumed. Thus, on the one hand these examples serve as counter examples to common beliefs and on the other hand serve as a guideline for future work.
|
|
| 7. |
- Abdelraheem, Mohamed, et al.
(författare)
-
Practical Attacks on Relational Databases Protected via Searchable Encryption
- 2018
-
Ingår i: Lecture Notes in Computer Science. - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. - 9783319991351 ; , s. 171-191
-
Konferensbidrag (refereegranskat)abstract
- Searchable symmetric encryption (SSE) schemes are commonly proposed to enable search in a protected unstructured documents such as email archives or any set of sensitive text files. However, some SSE schemes have been recently proposed in order to protect relational databases. Most of the previous attacks on SSE schemes have only targeted its common use case, protecting unstructured data. In this work, we propose a new inference attack on relational databases protected via SSE schemes. Our inference attack enables a passive adversary with only basic knowledge about the meta-data information of the target relational database to recover the attribute names of some observed queries. This violates query privacy since the attribute name of a query is secret.
|
|
| 8. |
- Abed, F., et al.
(författare)
-
Optimal coordination mechanisms for multi-job scheduling games
- 2014
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783662447765 ; 8737, s. 13-24
-
Konferensbidrag (refereegranskat)abstract
- We consider the unrelated machine scheduling game in which players control subsets of jobs. Each player's objective is to minimize the weighted sum of completion time of her jobs, while the social cost is the sum of players' costs. The goal is to design simple processing policies in the machines with small coordination ratio, i.e., the implied equilibria are within a small factor of the optimal schedule. We work with a weaker equilibrium concept that includes that of Nash. We first prove that if machines order jobs according to their processing time to weight ratio, a.k.a. Smith-rule, then the coordination ratio is at most 4, moreover this is best possible among nonpreemptive policies. Then we establish our main result. We design a preemptive policy, externality, that extends Smith-rule by adding extra delays on the jobs accounting for the negative externality they impose on other players. For this policy we prove that the coordination ratio is 1+φ≈2.618, and complement this result by proving that this ratio is best possible even if we allow for randomization or full information. Finally, we establish that this externality policy induces a potential game and that an ε-equilibrium can be found in polynomial time. An interesting consequence of our results is that an ε-local optima of R| |∑w j C j for the jump (a.k.a. move) neighborhood can be found in polynomial time and are within a factor of 2.618 of the optimal solution. The latter constitutes the first direct application of purely game-theoretic ideas to the analysis of a well studied local search heuristic.
|
|
| 9. |
- Abel, Andreas, 1974, et al.
(författare)
-
A formalized proof of strong normalization for guarded recursive types
- 2014
-
Ingår i: Lecture Notes in Computer Science: 12th Asian Symposium on Programming Languages and Systems, APLAS 2014 Singapore, 17-19 November 2014. - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349. - 9783319127354 ; 8858, s. 140-158
-
Konferensbidrag (refereegranskat)abstract
- We consider a simplified version of Nakano’s guarded fixed-point types in a representation by infinite type expressions, defined coinductively. Smallstep reduction is parametrized by a natural number “depth” that expresses under how many guards we may step during evaluation. We prove that reduction is strongly normalizing for any depth. The proof involves a typed inductive notion of strong normalization and a Kripke model of types in two dimensions: depth and typing context. Our results have been formalized in Agda and serve as a case study of reasoning about a language with coinductive type expressions.
|
|
| 10. |
- Abel, Andreas, 1974
(författare)
-
Compositional coinduction with sized types
- 2016
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349.
-
Konferensbidrag (refereegranskat)
|
|
