Dansk
DTU.dk
Index
Contact
Phone book
Internal Pages
DTU Alumni
Søgeord
Education
Education
MSc degree programme
PhD programmes
IMM courses
Coursebase DTU
Laboratories
Summer Schools
Welcome to DTU
DTU Informatics bookshop
Research
Research
Research areas
Algorithms and Logic
Cognitive Systems
Data Analysis
Dynamical Systems
---
Image Analysis & Computer Graphics
Language-Based Technology
Mathematical Statistics
Scientific Computing
Software Engineering
Research centers
Publications
Industrial collaboration
Industrial collaboration
Public sector consultancy
Advanced Technology Foundation Projects
Continuing education
Model-based Software Engineering Center
MT-Lab
PhD education
Software Development Center
Statistical Consulting Center
About DTU Informatics
About DTU Informatics
Contact
Employees
Facts about DTU Informatics
Getting to DTU Informatics
Advisory Board
Information material
Find the expert
Organisation
Vision
Available jobs
Library
Portalen DTU
Alumni association (in Danish)
News
News
Latest news
News Archive at DTU Informatics
Calendar at DTU Informatics
English
>
Research
>
Language-Based Technology
>
Group Members
Print
Research areas
Algorithms and Logic
Cognitive Systems
Data Analysis
Dynamical Systems
Embedded Systems Engineering
Image Analysis & Computer Graphics
Language-Based Technology
Research
Software
Teaching
Group Members
Publications
Mathematical Statistics
Scientific Computing
Software Engineering
Research centers
Publications
Title:
Observation Predicates in Flow Logic
Type:
ReportReport
Participant(s):
Author:
Nielson, Flemming
(Cwisno: 9539)
Technical University of Denmark
Email:
---
Author:
Nielson, Hanne Riis
(Cwisno: 9540)
Technical University of Denmark
Email:
---
Forfatter: Sun, Hongyan
Technical University of Denmark
Abstract:
Motivated by the connection between strong and soft type systems we explore flow analyses with hard constraints on the admissible solutions. We show how to use observation predicates and formula rearrangements to map flow analyses with hard constraints into more traditional flow analyses in such a way that the hard constraints are satisfi ed exactly when the observation predicates report no violations. The development is carried out in a large fragment of a first order logic with negation and also takes care of the transformations necessary in order to adhere to the stratification restrictions inherent in Alternation-free Least Fixed Point Logic and similar formalisms such as Datalog.
Published:
File(s):
imm2812.pdf
See the publication in DTU Orbit
Top
Matematiktorvet
DTU - Building 303B
DK-2800 Kgs. Lyngby
---
Tel +45 4525 3031
EAN 5798000428515
Cookies