| 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. |
- Abel, Andreas, 1974, et al.
(författare)
-
Verifying a semantic βη-conversion test for martin-löf type theory
- 2008
-
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. - 9783540705932 ; 5133 LNCS, s. 29-56
-
Konferensbidrag (refereegranskat)abstract
- Type-checking algorithms for dependent type theories often rely on the interpretation of terms in some semantic domain of values when checking equalities. Here we analyze a version of Coquand's algorithm for checking the βη-equality of such semantic values in a theory with a predicative universe hierarchy and large elimination rules. Although this algorithm does not rely on normalization by evaluation explicitly, we show that similar ideas can be employed for its verification. In particular, our proof uses the new notions of contextual reification and strong semantic equality. The algorithm is part of a bi-directional type checking algorithm which checks whether a normal term has a certain semantic type, a technique used in the proof assistants Agda and Epigram. We work with an abstract notion of semantic domain in order to accommodate a variety of possible implementation techniques, such as normal forms, weak head normal forms, closures, and compiled code. Our aim is to get closer than previous work to verifying the type-checking algorithms which are actually used in practice.
|
|
| 3. |
|
|
| 4. |
- Adams, Robin, 1978
(författare)
-
Formalized metatheory with terms represented by an indexed family of types
- 2006
-
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. ; 3839, s. 1-16
-
Konferensbidrag (refereegranskat)abstract
- It is possible to represent the terms of a syntax with binding constructors by a family of types, indexed by the free variables that may occur. This approach has been used several times for the study of syntax and substitution, but never for the formalization of the metatheory of a typing system. We describe a recent formalization of the metatheory of Pure Type Systems in Coq as an example of such a formalization. In general, careful thought is required as to how each definition and theorem should be stated, usually in an unfamiliar ‘big-step’ form; but, once the correct form has been found, the proofs are very elegant and direct.
|
|
| 5. |
- Adams, Robin, 1978, et al.
(författare)
-
Weyl's predicative classical mathematics as a logic-enriched type theory
- 2007
-
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. ; 4502, s. 1-17
-
Konferensbidrag (refereegranskat)abstract
- In Das Kontinuum, Weyl showed how a large body of classical mathematics could be developed on a purely predicative foundation. We present a logic-enriched type theory that corresponds to Weyl’s foundational system. A large part of the mathematics in Weyl’s book — including Weyl’s definition of the cardinality of a set and several results from real analysis — has been formalised, using the proof assistant Plastic that implements a logical framework. This case study shows how type theory can be used to represent a non-constructive foundation for mathematics.
|
|
| 6. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
A Verification System for Distributed Objects with Asynchronous Method Calls
- 2009
-
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. - 9783642103728 ; 5885, s. 387-406
-
Konferensbidrag (refereegranskat)abstract
- We present a verification system for Creol, an object-orientedmodeling language for concurrent distributed applications.The system is an instance of KeY, a framework for object oriented software verification, which has so far been applied foremost to sequential Java. Building on KeY characteristic concepts, like dynamic logic, sequent calculus, explicit substitutions, and the taclet rule language, the system presented in this paper addresses functional correctness of Creol models featuring local cooperative thread parallelism and global communication via asynchronous method calls. The calculus heavily operates on communication histories which describe the interfaces of Creol units. Two example scenarios demonstrate the usage of the system.
|
|
| 7. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
Abstract Object Creation in Dynamic Logic - To Be or Not To Be Created
- 2009
-
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. - 9783642050886 ; 5850, s. 612 - 627
-
Konferensbidrag (refereegranskat)abstract
- In this paper we give a representation of a weakest precondition calculus for abstract object creation in dynamic logic, the logic underlying the KeY theorem prover. This representation allows to both specify and verify properties of objects at the abstraction level of the (object-oriented) programming language. Objects which are not (yet) created never play any role, neither in the specification nor in the verification of properties. Further, we show how to symbolically execute abstract object creation.
|
|
| 8. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
Automatic Validation of Transformation Rules for Java Verification against a Rewriting Semantics
- 2005
-
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. - 354030553X ; LNCS 3835, s. 412 - 426
-
Konferensbidrag (refereegranskat)abstract
- This paper presents a methodology for automatically validating program transformation rules that are part of a calculus for Java source code verification. We target the Java Dynamic Logic calculus which is implemented in the interactive prover of the KeY system. As a basis for validation, we take an existing SOS style rewriting logic semantics for Java, formalized in the input language of the Maude system. That semantics is `lifted' to cope with schematic programs like the ones appearing in program transformation rules. The rewriting theory is further extended to generate valid initial states for involved program fragments, and to check the final states for equivalence. The result is used in frequent validation runs over the relevant fragment of the calculus in the KeY system.
|
|
| 9. |
- Alexandersson, Ruben, 1975, et al.
(författare)
-
Implementing Fault Tolerance Using Aspect Oriented Programming
- 2007
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - 1611-3349 .- 0302-9743. - 9783540752936 ; 4746/2007, s. 57-74
-
Konferensbidrag (refereegranskat)abstract
- Aspect oriented programming (AOP) is a promising technique for implementing fault tolerance. Still there exist few actual implementations. One reason is that most present day AOP languages do not offer the level of control needed. This paper addresses the problem by defining a representative set of fault tolerance mechanisms. The set can be used for evaluating the feasibility of languages and for finding needs for improvements. It has been used to evaluate the AspectC++ language, and a number of limitations have been revealed. AspectC++ was then extended in order to address this. It is also demonstrated how reusable fault tolerance mechanisms can be built using aspect oriented C++, and the advantages compared to using standard C++ are discussed.
|
|
| 10. |
- Allwood, Jens, et al.
(författare)
-
Modeling embodied feedback with virtual humans
- 2008
-
Ingår i: Lecture Notes in Computer Science. - Berlin, Heidelberg : Springer. - 0302-9743 .- 1611-3349. - 9783540790365 ; 4930
-
Tidskriftsartikel (refereegranskat)
|
|
