002: The Yogi Project: Software Property Checking via Static Analysis and Testing Nori, Aditya; Thakur, Aditya; Tetali, Saideep; Rajamani, Sriram
007: Parametric Trace Slicing and Monitoring
Chen, Feng; Rosu, Grigore
015: Alpaga: A Tool for Solving Parity Games with Imperfect Information Doyen, Laurent; Berwanger, Dietmar; Chatterjee, Krishnendu; De Wulf, Martin; Henzinger, Thomas A.
016: ITPN-PerfBound: A performance bound tool for Interval Time Petri Nets Pacini, Elina Rocio; Bernardi, Simona; Gribaudo, Marco
017: Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays Brummayer, Robert Daniel; Biere, Armin
022: MoonWalker: verification of .NET programs Ruys, Theo; Aan de Brugh, Niels H.M.; Nguyen, Viet Yen
028: Falsification of LTL Safety Properties in Hybrid Systems
Plaku, Erion; Kavraki, Lydia; Vardi, Moshe
032: Ground Interpolation for the Theory of Equality Krstic, Sava; Fuchs, Alexander; Goel, Amit; Grundy, Jim; Tinelli, Cesare
033: All-Termination(T)
Turon, Aaron; Manolios, Panagiotis
043: Test input generation for programs with pointers
Vanoverberghe, Dries; Tillmann, Nikolai; Piessens, Frank
044: Compositional Predicate Abstraction from Game Semantics
Ghica, Dan; Bakewell, Adam
048: Memoised Garbage Collection for Software Model Checking
Nguyen, Viet Yen; Ruys, Theo
051: Compositional Synthesis of Reactive Systems from Live Sequence Chart Specifications Segall, Itai; Kugler, Hillel
065: Computing Optimized Representations for Non-Convex Polyhedra by Detection and Removal of Redundant Linear Constraints Disch, Stefan; Scholl, Christoph; Pigorsch, Florian; Kupferschmid, Stefan
073: Static Analysis Techniques for Parameterised Boolean Equation Systems Willemse, Tim; Orzan, Simona; Wesselink, Wieger
082: Semantic Reduction of Thread Interleavings for Concurrent Programs
Gupta, Aarti; Kahlon, Vineet; Sankaranarayanan, Sriram
084: Computing Weakest Strategies for Safety Games of Imperfect Information Kuijper, Wouter; Pol, Jaco
085: Buechi Complementation and Size-Change Termination
Fogarty, Seth; Vardi, Moshe
086: Path Feasibility Analysis for String-Manipulating Programs
Bjorner, Nikolaj; Tillmann, Nikolai; Voronkov, Andrei
088: TaPAS : The Talence Presburger Arithmetic Suite
Leroux, Jerome; Point, Gerald
91: Satisfiability Procedures for Combination of Theories Sharing
Integer Offsets
Ringeissen, Christophe; Nicolini, Enrica; Rusinowitch, Michael
094: Hierarchical Adaptive State Space Caching based on Level Sampling
Wijs, Anton; Mateescu, Radu
095: Transition-based Directed Model Checking Kupferschmid, Sebastian; Wehrle, Martin; Podelski, Andreas
101: Context-bounded analysis for concurrent programs with dynamic creation of threads Atig, Mohamed Faouzi; Bouajjani, Ahmed; Qadeer, Shaz
113: Romeo : A Parametric Model-Checker for Petri Nets with Stopwatches Traonouez, Louis-Marie; Lime, Didier; Roux, Olivier (H.); Seidner, Charlotte
117: Verifying Reference Counting Implementations Emmi, Michael; Kohler, Eddie; Jhala, Ranjit; Majumdar, Rupak
118: RBAC-PAT: A Policy Analysis Tool for Role Based Access Control Yang, Ping; Stoller, Scott; Zhang, Yingbin; Solomon, Ayla; Luo, Ruiqi; Gofman, Mikhail
120: Hierachical Set Decision Diagrams and Regular Models Thierry-Mieg, Yann; Poitrenaud, Denis; Hamez, Alexandre; Kordon, Fabrice
137: Inferring Synchronization under Limited Observability Yorsh, Greta; Yahav, Eran; Vechev, Martin
141: Learning Minimal Separating DFA's for Compositional Verification Chen, Yu-Fang; larke, Edmund; Farzan, Azadeh; Tsay, Yih-Kuen; Wang, Bow-Yaw
144: An Efficient Invariant Generator
Majumdar, Rupak; Gupta, Ashutosh; Rybalchenko, Andrey
146: Specification Mining With Few False Positives Le Goues, Claire; Weimer, Westley
149: Symbolic String Verification: Combining String Analysis and Size Analysis Yu, Fang; Ibarra, Oscar H.; Bultan, Tevfik
160: The Complexity of Predicting Atomicity Violations Farzan, Azadeh; Parthasarathy, Madhusudan
169: Iterating Octagons
IOSIF, Radu; Bozga, Marius; Girlea, Codruta
2008年12月20日星期六
tacas 09 accepted papers
2008年11月6日星期四
centos 5.2 dont include g++ by default installation
While I compile zchaff sat solver under centos 5.2, it complain that dont find g++. it is actually in gcc-c++-4.1.2-42.el5.x86_64.rpm. just install it and everything ok
exploring similarity between sub constructor
there are some degree of similarity between sub constructors, and some operation only care such similarity, and dont care the difference.
for example, in a verilog parser, there is a data onstructor like this,
and blocking_assignment =
T_blocking_assignment_direct of lvalue*expression
| T_blocking_assignment_delay of lvalue*expression*delay_control
| T_blocking_assignment_event of lvalue*expression*event_control
and non_blocking_assignment =
T_non_blocking_assignment_direct of lvalue*expression
| T_non_blocking_assignment_delay of lvalue*expression*delay_control
| T_non_blocking_assignment_event of lvalue*expression*event_control
and in one operation regs, I only need to get the left value list, so I only care lvalue part,
In another operation deps, I only need to get the variables appear on right hand side, so I only need the expression part.
So can we just specify lvalue and expression without mention the exact constructor name and other data?
for example, in a verilog parser, there is a data onstructor like this,
and blocking_assignment =
T_blocking_assignment_direct of lvalue*expression
| T_blocking_assignment_delay of lvalue*expression*delay_control
| T_blocking_assignment_event of lvalue*expression*event_control
and non_blocking_assignment =
T_non_blocking_assignment_direct of lvalue*expression
| T_non_blocking_assignment_delay of lvalue*expression*delay_control
| T_non_blocking_assignment_event of lvalue*expression*event_control
and in one operation regs, I only need to get the left value list, so I only care lvalue part,
In another operation deps, I only need to get the variables appear on right hand side, so I only need the expression part.
So can we just specify lvalue and expression without mention the exact constructor name and other data?
2008年11月5日星期三
disabling of mihuo protocol
I use amule to download resource of verycd, but it just refuse to start, and complain about low ID,
I notice that there are mihuo protocol setting, so I just disable it , and everything OK
I notice that there are mihuo protocol setting, so I just disable it , and everything OK
2008年11月4日星期二
formal method to warn us about the effect of updated environment
When we or other people other then we, modify some code incrementally, then it will afect the proper treatment of the other code, so can we develop a metnod to warn us about what to do when it is need?
bridge the gap of my mind and the state of the art library
When we try to use a library, we has some idea about its functionality and structrue in our mind, which can be seen as an abstraction of the library.
So if there exist a method to connect this our mind with the actual lib?
So if there exist a method to connect this our mind with the actual lib?
2008年10月29日星期三
ICSE 08:ReBA: Refactoring-aware Binary Adaptation of Evolving Libraries
This paper propose to synthesis a compatible layer on new version library,to make the old code run correctly.
This idea is also in my mind for a long time.
This idea is also in my mind for a long time.
Incremental State-Space Exploration for Programs with Dynamically Allocated Data
OH,another idea that pop up in my mind but have not followed.
This paper deal with increamental state space exploration for Programs with Dynamically Allocated Data
This paper deal with increamental state space exploration for Programs with Dynamically Allocated Data
Answering Conceptual Queries with Ferret
This define a frame work to expresse the relation between varais information object in software development env, and use correlation to answer the desire result. somewhat similar to previous "Jungloid Mining: Helping to Navigate the API Jungle"
2008年10月27日星期一
Bidirectionalization for Free
Oww, my god, this idea is also in my mind for a long time.
Can we just write the encoder , and generate a decoder automatically?
If use verilog, such an paper can be submitted to both dac and cav and popl.
this is also related to counterexample directed synthesis.
Can we just write the encoder , and generate a decoder automatically?
If use verilog, such an paper can be submitted to both dac and cav and popl.
this is also related to counterexample directed synthesis.
A Cost Semantics for Self-Adjusting Computation
Self-Adjusting Computation seems to be somewhat very hot, from 2006.
It focus on computing result with delta.
find Umut Acar
It focus on computing result with delta.
find Umut Acar
Local Rely-Guarantee Reasoning
So many people focus on combining separation logic and Rely-Guarantee.
I may need to dive into this
I may need to dive into this
Static Contract Checking for Haskell
Static Contract Checking for Haskell propose a contract checking method. This prove my long stand suspection that why not people do formal verification of functional language.
But according to curry howard corresponding, this is acutally not an insteresting topic, because those people who interest in formal verification all goto matrin lof .2008年10月26日星期日
State-Dependent Representation Independence
This paper and its related papers shown below, focus on such a problem that, if an general type system can be augmented by local state to further improve it precision without sacrify decidability?
So if this tech is a special case of my idea that combine cheap hinder-milner type system in clasical ML with an expensive counterexample guided refinement based type inference on those potential type error?
For example, a type T has 2 type constructor A and B, for a list of element T, I filter out all those with constructor A, to generate a list l_A, so when enumerating l_A, I only need to process constructor A,not for B.
I general ML, this will raise an incomplete warning, but I can rule it out with refinement.
Ahmed. Step-indexed syntactic logical relations for recursive and quantified types.
Syntactic logical relations for polymorphic and recursive types
Recursive polymorphic types and parametricity in an operational framework.
Typed operational reasoning.
Selective strictness and parametricity in structural operational semantics, inequationally.
So if this tech is a special case of my idea that combine cheap hinder-milner type system in clasical ML with an expensive counterexample guided refinement based type inference on those potential type error?
For example, a type T has 2 type constructor A and B, for a list of element T, I filter out all those with constructor A, to generate a list l_A, so when enumerating l_A, I only need to process constructor A,not for B.
I general ML, this will raise an incomplete warning, but I can rule it out with refinement.
Ahmed. Step-indexed syntactic logical relations for recursive and quantified types.
Syntactic logical relations for polymorphic and recursive types
Recursive polymorphic types and parametricity in an operational framework.
Typed operational reasoning.
Selective strictness and parametricity in structural operational semantics, inequationally.
a good survey of Mixed Transition Systems
A vmcai 09 paper by "Mixed Transition Systems Revisited" Ou Wei , Arie Gurfinkel , and Marsha Chechik.
2008年10月25日星期六
usb device not recognized on CentOS 5.2 over dell inspiron 531
I install CentOS 5.2 on my Dell Inspiron 531, everything is OK except that sometimes it will refuse to recognize the USB mass storage devide, and dmesg says that "usb device not address XX , error -100".
I finally resolve this by rmmod ehci_hcd, and then the device will be automaticly recognized and mounted.
I think this may be because that the ehci_hcd is stand in the way of the other proper handler of usb devide.
I finally resolve this by rmmod ehci_hcd, and then the device will be automaticly recognized and mounted.
I think this may be because that the ehci_hcd is stand in the way of the other proper handler of usb devide.
2008年10月24日星期五
porting/using the state of the art applications in web framework
How can I use state of the art program, such as pdf render, in web framework, with only minor modification?
2008年10月23日星期四
can type system be dynamic?
In logic community, abstraction can be refined.
Type system , especially dependent type, corresponding to abstraction, so can they be make to be refined?
Type system , especially dependent type, corresponding to abstraction, so can they be make to be refined?
2008年10月21日星期二
primitive recursion and general recursion
The primitive one must be constructed by zero, successor, projection, composition and primitive recursion function.
The idea of primitive recursion function is : for a list of variables that can be induction, induct on them one by one, not jumping to next one before the current one reach the base case.
primitive recursion function is only a subset of (general) recursive function(or computable one), some function like Ackman is (general) recursive, but not primitive one.
Here give an excellent proof if this.
The idea of primitive recursion function is : for a list of variables that can be induction, induct on them one by one, not jumping to next one before the current one reach the base case.
primitive recursion function is only a subset of (general) recursive function(or computable one), some function like Ackman is (general) recursive, but not primitive one.
Here give an excellent proof if this.
2008年10月20日星期一
Handbook of Automated Reasoning
Volume 1
- John Alan Robinson, Andrei Voronkov: Preface. BibTeX
- Leo Bachmair, Harald Ganzinger: Resolution Theorem Proving(can be find on citeseerX). 19-99 BibTeX
- Reiner Hähnle: Tableaux and Related Methods. 100-178 BibTeX
- Anatoli Degtyarev, Andrei Voronkov: The Inverse Method(can be find on citeseerX). 179-272 BibTeX
- Matthias Baaz, Uwe Egly, Alexander Leitsch: Normal Form Transformations. 273-333 BibTeX
- Franz Baader, Wayne Snyder: Unification Theory.(can be find on citeseerX) 445-532 BibTeX
- Nachum Dershowitz, David A. Plaisted: Rewriting. 535-610 BibTeX
- Shang-Ching Chou, Xiao-Shan Gao: Automated Reasoning in Geometry. 707-749 BibTeX
- Alexander Bockmayr, Volker Weispfenning: Solving Numerical Constraints. 751-842 BibTeX
- Hubert Comon: Inductionless Induction. 913-962 BibTeX
Volume 2
Chapter 15- Peter B. Andrews: Classical Type Theory. 965-1007 BibTeX
- Frank Pfenning: Logical Frameworks. 1063-1147 BibTeX
- Jürgen Dix, Ulrich Furbach, Ilkka Niemelä: Nonmonotonic Reasoning: Towards Efficient Calculi and Implementations. 1241-1354 BibTeX
- Matthias Baaz, Christian G. Fermüller, Gernot Salzer: Automated Deduction for Many-Valued Logics. 1355-1402 BibTeX
- Hans Jürgen Ohlbach, Andreas Nonnengart, Maarten de Rijke, Dov M. Gabbay: Encoding Two-Valued Nonclassical Logics in Classical Logic. 1403-1486 BibTeX
- Arild Waaler: Connections in Nonclassical Logics. 1487-1578 BibTeX
- Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Daniele Nardi: Reasoning in Expressive Description Logics. 1581-1634 BibTeX
- Edmund M. Clarke, Bernd-Holger Schlingloff: Model Checking. 1635-1790 BibTeX
- Christian G. Fermüller, Alexander Leitsch, Ullrich Hustadt, Tanel Tammet: Resolution Decision Procedures. 1791-1849 BibTeX
- I. V. Ramakrishnan, R. C. Sekar, Andrei Voronkov: Term Indexing. 1853-1964 BibTeX
- Christoph Weidenbach: Combining Superposition, Sorts and Splitting. 1965-2013 BibTeX
- Reinhold Letz, Gernot Stenz: Model Elimination and Connection Tableau Procedures. 2015-2114 BibTeX
2008年10月19日星期日
type system list
I has investigate the relation between varias type system for a long time, and finally find the lambda cube is a good way to explain all these mess.
Hindley-Milner: it is restricted version of system F, this is the last one that has type inference. even system F dont has this ability. traditional ML such as haskell 98 and ocaml all based on this.
System F: ploy extendtion of simply typed typed calculus. As a whole it dont has type infenrece. GHC based on this.
There is a hierarchical familay of system F, where
F1 is just the simply typed typed calculus.
and any Fn is actually map from lowwer level to type. and Fw is the union of Fn.
- untyped lamda calculus
- simply typed typed calculus: extend untyped one with type, to avoid the paradox that a set refer to itself
- Terms depending on types, or polymorphism (as in System F),
- Types depending on types, or type operators, and
- Types depending on terms, or dependent types (as in LF).
Hindley-Milner: it is restricted version of system F, this is the last one that has type inference. even system F dont has this ability. traditional ML such as haskell 98 and ocaml all based on this.
System F: ploy extendtion of simply typed typed calculus. As a whole it dont has type infenrece. GHC based on this.
There is a hierarchical familay of system F, where
F1 is just the simply typed typed calculus.
and any Fn is actually map from lowwer level to type. and Fw is the union of Fn.
Hindley–Milner type inference algorithm
Hindley–Milner is a polymorphic extention of simply typed lamda calculus, weaker than system F. It is also the name of type inference algorithm is this type system.
This wiki page give its basic principle. The basic principle is that first use some type variable and semantic of abstraction and application to generate a list of type constraint, and then use unification to solve it. In one world, to find the most general type setting to satisfy the list of type constraint.
Here is the implementation of Hindley–Milner in perl language. it is based on Basic Polymorphic Typechecking.
This wiki page give its basic principle. The basic principle is that first use some type variable and semantic of abstraction and application to generate a list of type constraint, and then use unification to solve it. In one world, to find the most general type setting to satisfy the list of type constraint.
Here is the implementation of Hindley–Milner in perl language. it is based on Basic Polymorphic Typechecking.
pointer type
I shoudl enforce the typing rules on pointer, such that it can't be use improperly, by:
In this way, pointer for two memory block will run in separation logic semantic
Somewhat like tagged mameory .
- use special type tag to distinguish poniter from other object, such as integer and float , even from other pointer
- pointer shoudl only be created by special operators, and a special type tag will be attached to it. pointer created by two operator will has different type tag
- pointer can only be added or sub some const from it, and still preserve its type.
In this way, pointer for two memory block will run in separation logic semantic
Somewhat like tagged mameory .
2008年10月18日星期六
yet another learn on dependent type
dependent type is actually a type that depend on a value. There are three level of dependent type:
- first order, include the dependent product type into simple typed lamda calculus. this make it to be system LF
- second order , allow quantification over type constructor
- higher order, this allow all four forms of abstraction from the lambda cube: functions from terms to terms, types to types, terms to types and types to terms. The system corresponds to the Calculus of constructions.this is coq now.
Some issue that may interference with my idea on regular enumeration
- implicte variable in agda, HAHA, actually this is to omit the type declaration for the parameter in dependent type
- find carefully in ocaml haskell agda coq and epigam for it
- try to figure out a small ML language as our base, or just to invent a new one
Curry-Howard correspondence
Curry-Howard correspondence is simply the corresponding between proof and type system. That is :a proof is a program, the formula it proves is a type for the program.
It relate two fields that seem unrelated: proof theory and computability theory. The previous one contain simply typed lamda caculus, Martin lof and CIC, and so on. The latter one contain pushdown automata, turing machine, and so on.
This wiki page also provide an interesting idea:
________________________
can we imagine a typed version of Turing machine that would behave as a proof system? Typed assembly languages are such an instance of "low-level" model of computation that carries types.
________________________
(*this table come from wikipedia*)
product type is just the tuple notation, and sum type is just like HASKELL sub type constructor, for example:
___________________________
It relate two fields that seem unrelated: proof theory and computability theory. The previous one contain simply typed lamda caculus, Martin lof and CIC, and so on. The latter one contain pushdown automata, turing machine, and so on.
This wiki page also provide an interesting idea:
________________________
can we imagine a typed version of Turing machine that would behave as a proof system? Typed assembly languages are such an instance of "low-level" model of computation that carries types.
________________________
This correspondence can be considered in two level:
- at the formula and type level that dont consider the detail of proof system and type system
- at the proof and program level that consider detail of proof system and type system
At the formula and type level, we has following correspondence:
| Logic side | Programming side | |
|---|---|---|
| Curry-style typing | Church-style typing | |
| universal quantification | intersection type | dependent product type |
| existential quantification | union type | dependent sum type |
| implication | function type | |
| conjunction | product type | |
| disjunction | sum type | |
| true formula | unit type | |
| false formula | bottom type | |
product type is just the tuple notation, and sum type is just like HASKELL sub type constructor, for example:
___________________________
datatype tree = Leaf
| Node of (int * tree * tree)
______________________________
At the level of proof systems and models of computations,
| Logic side | Programming side | ||
|---|---|---|---|
| Hilbert-style deduction system |
| ||
| natural deduction |
|
(*this table come from wikipedia*)
Hilbert system use large numbers of axioms, and little number or even only one rule, the modus ponens.
Programming in Martin-Löf's Type Theory
This book is a fairly good introduction to Martin-Löf's Type Theory . It is worth reading.
VMCAI 09 : Reducing Behavioural to Structural Properties of Programs with Procedures
This paper try to figure out structrue information from behavior, just reverse the traditinal working direction. One of his sentense best describe the difference between behaviour and structure:
-------------------------------
Both program structure and behaviour can be speci ed by temporal logicformulae: structural properties concern the textual sequencing of instructions ina program, while behavioural properties consider their executional sequencing.
-------------------------------
In it definition if structure and behavior in section 2, I notice that the behaviour model record the state of stack, while the structure model only contain flow graph.
It major application is in compositional verification, in another word, to synthesis the invaraint of outer world.
BTW: it remind me of the "path invariant" paper on PLDI07, which represent the counterexample as a program. Can this be think of as another form of behavior(counterexample) to structure(program)???
-------------------------------
Both program structure and behaviour can be speci ed by temporal logicformulae: structural properties concern the textual sequencing of instructions ina program, while behavioural properties consider their executional sequencing.
-------------------------------
In it definition if structure and behavior in section 2, I notice that the behaviour model record the state of stack, while the structure model only contain flow graph.
It major application is in compositional verification, in another word, to synthesis the invaraint of outer world.
BTW: it remind me of the "path invariant" paper on PLDI07, which represent the counterexample as a program. Can this be think of as another form of behavior(counterexample) to structure(program)???
2008年10月17日星期五
VMCAI 09: Shape-value Abstraction for Verifying Linearizability
This paper use the hotly researched method that combine rely guarantee with separation logic, to verify the concurrent program with memory alloc and dealloc.
Traditinal approaches all depend on reachable analysis, which require a bounded thread number, while this paper use theorem proving approach.
These days, all guys become more and more smart on using theorem proving technology, :)
This is his web site.
What? I found that this paper require user to annotate the code with linearization point, and also need the user to give the semantic of atomic operation in separation logic style.
But one delight point is that this paper dont abstract away the value store in the data structure, as other method do. In this way, some more useful problem can be solved.
BTW: In his previous paper that firstly combine rely/guarentee with seperation logic, there is a concept of stablity, which says something should persist after execut some action, which remind me of the inductive invaraint.
One more notice, this guy also provide ocaml source code on web site.
Traditinal approaches all depend on reachable analysis, which require a bounded thread number, while this paper use theorem proving approach.
These days, all guys become more and more smart on using theorem proving technology, :)
This is his web site.
What? I found that this paper require user to annotate the code with linearization point, and also need the user to give the semantic of atomic operation in separation logic style.
But one delight point is that this paper dont abstract away the value store in the data structure, as other method do. In this way, some more useful problem can be solved.
BTW: In his previous paper that firstly combine rely/guarentee with seperation logic, there is a concept of stablity, which says something should persist after execut some action, which remind me of the inductive invaraint.
One more notice, this guy also provide ocaml source code on web site.
Inital consideration for regular data structure enumaration
I think we may do this topic in a step by step way:
In the first step, we still persist to static type, we only use regular expression to enumerate to a certain sub constructor with known name, the compiler will try to figure out the actual and complete sub constructor enumerate process.
The goal of this idea is just to separate the data structure from program structure. Even if the library developer change the data structure significantly, we can still compile the old code.
In the first step, we still persist to static type, we only use regular expression to enumerate to a certain sub constructor with known name, the compiler will try to figure out the actual and complete sub constructor enumerate process.
The goal of this idea is just to separate the data structure from program structure. Even if the library developer change the data structure significantly, we can still compile the old code.
VMCAI 09: LTL Generalized Model Checking Revisited
Generalized Model Checking is the mixtrue of MC with game semantic, that is , something is unfixed, and GMC try to find out definition of these unfixed entities, or decide if such definition exist, such that the concrete MC or satisfiability problom can be solved.
This topic remind me of the synthesis and fix problem, which also has some thing left to be defined.
This topic remind me of the synthesis and fix problem, which also has some thing left to be defined.
2008年10月16日星期四
Design OS with full FL or Fl sematics
Can we use Fl to build a OS , or build a OS with FL semantic with any language you like?
In this way, reasoning of OS will be much easier.
In fact, the value of FL is to force people to think in Fl way, which is easier to be reasoned.
In this way, reasoning of OS will be much easier.
In fact, the value of FL is to force people to think in Fl way, which is easier to be reasoned.
ICFP 08 : NixOS: A Purely Functional Linux Distribution
We all had suffer from "DLL hell" problem previously, which occur when you install a new software, which come with a buggy DLL file with newer version than the old one in the OS. After installation, some old software that use old DLL will fail to function. This is due to the stateful management of system configuration, which will generate side effect that will affect other component in system.
This paper propose a new idea that dynamicly generate the system setting for the software seperatly, which will not be seen by other program, much similar to program in FL.
There are no any global setting such as /bin /etc /proc in NixOX any more , only /bin/sh persist. Any program installation will contain his own related lib and other program, which will reside in a seperated place unvisible to other program.
This paper also propose a FL style language to replace counterpart in RPM and apt, to specify the dependency and method to resolve dependence.
It is some what like a virtual machine, with very low overhead.
This paper propose a new idea that dynamicly generate the system setting for the software seperatly, which will not be seen by other program, much similar to program in FL.
There are no any global setting such as /bin /etc /proc in NixOX any more , only /bin/sh persist. Any program installation will contain his own related lib and other program, which will reside in a seperated place unvisible to other program.
This paper also propose a FL style language to replace counterpart in RPM and apt, to specify the dependency and method to resolve dependence.
It is some what like a virtual machine, with very low overhead.
ICFP 2008 paper's link
ICFP 2008 : The 13th ACM SIGPLAN International Conference on Functional Programming
Final Program
Invited Talk (chair: Peter Thiemann)
9:00 Lazy and Speculative Execution in Computer Systems
Butler Lampson;
Microsoft Research
Session 1 (chair: Martin Sulzmann)
10:30 Flux: FunctionaL Updates for XML
James Cheney;
University of Edinburgh
10:55 Typed Iterators for XML
Giuseppe Castagna1 and Kim Nguyen2;
1PPS (CNRS) - Université Paris 7 - Paris, France, 2LRI - Université Paris-Sud 11 - Orsay, France
Session 2 (chair: Matthew Fluet)
11:50 Aura: A Programming Language for Authorization and Audit
Limin Jia, Jeffrey Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph Schorr, Steve Zdancewic;
University of Pennsylvania
12:15 The Power of Pi
Nicolas Oury and Wouter Swierstra;
University of Nottingham
Session 3 (chair: Ralf Hinze)
14:00 Type Checking with Open Type Functions
Tom Schrijvers1, Simon Peyton Jones2, Manuel Chakravarty3, Martin Sulzmann4;
1K.U.Leuven, 2Microsoft Research Cambridge, 3UNSW, Sydney, 4ITU, Denmark
14:25 Graphic Type Constraints and Efficient Type Inference: from ML to MLF
Boris Yakobowski and Didier Remy;
INRIA
Session 4 (chair: Tim Sheard)
15:20 A Type-Preserving Compiler in Haskell
Louis-Julien Guillemette and Stefan Monnier;
Université
de Montréal
15:45 Experience Report: Playing the DSL Card, A Domain Specific Language for Component Configuration
Mark Jones;
Portland State University
16:05 Generic Discrimination--Sorting and Partitioning Unshared Data in Linear Time
Fritz Henglein;
DIKU, University of Copenhagen
Session 5 (chair: Norman Ramsey)
17:00 Transactional Events for ML
Laura Effinger-Dean, Matthew Kehrt, Dan Grossman;
University of Washington
17:25 Experience Report: Erlang in Acoustic Ray Tracing
Christian Convey1, Andrew Fredricks1, Christopher Gagner1, Douglas Maxwell1, Lutz Hamel2;
1Naval Undersea Warfare Centers, RI, USA, 2Dept. of Computer Science and Statistics, University of Rhode Island
17:45 Implicitly-threaded parallelism in Manticore
Matthew Fluet1, Mike Rainey2, John Reppy2, Adam Shaw2;
1Toyota Technological Institute at Chicago, 2University of Chicago
18:10 PC chair's report
Tuesday, September 23
Invited Talk (chair: James Hook)
9:00 Defunctionalized Interpreters for Higher-Order Languages
Olivier Danvy;
University of Aarhus
Session 6 (chair: Andrew Tolmach)
10:30 Parametric Higher-Order Abstract Syntax for Mechanized Semantics
Adam Chlipala;
Harvard University
10:55 Typed Closure Conversion Preserves Observational Equivalence
Amal Ahmed and Matthias Blume;
Toyota Technological Institute at Chicago
Session 7 (chair: Manuel Chakravarty)
11:50 Write it Recursively: A Generic Framework for Optimal Path Queries
Akimasa Morihata, Kiminori Matsuzaki, Masato Takeichi;
University of Tokyo
12:15 Efficient Nondestructive Equality Checking for Trees and Graphs
Michael D. Adams and R. Kent Dybvig;
Indiana University
Session 8 (chair: Zhenjiang Hu)
14:00 Functional Pearl: Streams and Unique Fixed Points
Ralf Hinze, University of Oxford
14:25 Data-Flow Testing of Declarative Programs PPT
Sebastian Fischer1 and Herbert Kuchen2;
1University of Kiel, 2University of Münster
Session 9 (chair: Andrew Kennedy)
15:20 Functional Translation of a Calculus of Capabilities
Arthur Charguéraud and François Pottier;
INRIA
15:45 Experience Report: Paradise: A Two-Stage DSL Embedded in Haskell
Lennart Augustsson, Howard Mansell, Ganesh Sittampalam;
Credit Suisse
16:05 Ynot: Reasoning with the Awkward Squad
Aleksandar Nanevski1, Greg Morrisett2, Avi Shinnar2, Paul Govereau2, Lars Birkedal3;
1Microsoft Research, Cambridge, 2Harvard University, 3IT University, Copenhagen
Session 10 (chair: Michael Sperber)
17:00 A Scheduling Framework for General-Purpose Parallel Languages
Matthew Fluet1, Michael Rainey2, John Reppy2;
1Toyota Technological Institute at Chicago, 2University of Chicago
17:25 Space Profiling for Parallel Functional Programs
Daniel Spoonhower1, Guy E. Blelloch1, Robert Harper1, Phillip B. Gibbons2;
1Carnegie Mellon University, 2Intel Reseach Pittsburgh
Awards and Announcements (chair: Kevin Millikin)
18:00 ICFP 2009 Announcement
Phil Wadler
18:10 Most Influential ICFP'98 Paper Award
Kathleen Fisher
18:20 Report on the Eleventh ICFP Programming Contest
Tim Sheard, Tim Chevalier, Chuan-kai Lin, Garrett Morris, Emerson Murphy-Hill, Andy Gill, John Reppy, Lars Bergstrom, Mike Rainey, Adam Shaw, Virgil Gheorghiu;
Portland State University, University of Chicago
Wednesday, September 24
Invited Talk (chair: Mitchell Wand)
9:00 Polymorphism and Page Tables--Systems Programming From a Functional Programmer's Perspective
Mark Jones;
Portland State University
Session 11 (chair: Fritz Henglein)
10:30 Pattern Minimization Problems over Recursive Data Types
Alexander Krauss;
TU München
10:55 Deciding kCFA is complete for EXPTIME
David Van Horn and Harry Mairson;
Brandeis University
Session 12 (chair: Derek Dreyer)
11:50 HMF: Simple Type Inference for First-Class Polymorphism
Daan Leijen;
Microsoft Research
12:15 FPH: First-class Polymorphism for Haskell
Dimitrios Vytiniotis1, Stephanie Weirich1, Simon Peyton Jones2;
1University of Pennsylvania, 2Microsoft Research
Session 13 (chair: Chung-chieh Shan)
14:00 Mixin' Up the ML Module System
Derek Dreyer and Andreas Rossberg;
MPI-SWS
14:25 Compiling Self-Adjusting Programs with Continuations
Ruy Ley-Wild1, Matthew Fluet2, Umut Acar2;
1Carnegie Mellon University, 2Toyota Technological Institute at Chicago
Session 14 (chair: Henrik Nilsson)
15:20 Flask: Staged Functional Programming for Sensor Networks
Geoffrey Mainland, Greg Morrisett, Matt Welsh;
Harvard University
15:45 Experience Report: A Pure Shirt Fits Reflections on Haskell at Bluespec
Ravi Nanavati;
Bluespec, Inc.
16:05 Functional Netlists
Sungwoo Park, Jinha Kim, Hyeonseung Im;
Pohang University of Science and Technology
Session 15 (chair: Kathleen Fisher)
17:00 NixOS: A Purely Functional Linux Distribution
Eelco Dolstra1 and Andres Löh2;
1Delft University of Technology, 2Utrecht University
17:25 Experience Report: Visualizing Data through Functional Pipelines
David Duke1, Rita Borgo1, Colin Runciman2, Malcolm Wallace2;
1University of Leeds, UK, 2University of York, UK
17:45 Quotient Lenses
J. Nathan Foster1, Alexandre Pilkiewicz2, Benjamin C. Pierce1;
1University of Pennsylvania, 2Ecole Polytechnique
Final Program
Invited Talk (chair: Peter Thiemann)
9:00 Lazy and Speculative Execution in Computer Systems
Butler Lampson;
Microsoft Research
Session 1 (chair: Martin Sulzmann)
10:30 Flux: FunctionaL Updates for XML
James Cheney;
University of Edinburgh
10:55 Typed Iterators for XML
Giuseppe Castagna1 and Kim Nguyen2;
1PPS (CNRS) - Université Paris 7 - Paris, France, 2LRI - Université Paris-Sud 11 - Orsay, France
Session 2 (chair: Matthew Fluet)
11:50 Aura: A Programming Language for Authorization and Audit
Limin Jia, Jeffrey Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph Schorr, Steve Zdancewic;
University of Pennsylvania
12:15 The Power of Pi
Nicolas Oury and Wouter Swierstra;
University of Nottingham
Session 3 (chair: Ralf Hinze)
14:00 Type Checking with Open Type Functions
Tom Schrijvers1, Simon Peyton Jones2, Manuel Chakravarty3, Martin Sulzmann4;
1K.U.Leuven, 2Microsoft Research Cambridge, 3UNSW, Sydney, 4ITU, Denmark
14:25 Graphic Type Constraints and Efficient Type Inference: from ML to MLF
Boris Yakobowski and Didier Remy;
INRIA
Session 4 (chair: Tim Sheard)
15:20 A Type-Preserving Compiler in Haskell
Louis-Julien Guillemette and Stefan Monnier;
Université
de Montréal
15:45 Experience Report: Playing the DSL Card, A Domain Specific Language for Component Configuration
Mark Jones;
Portland State University
16:05 Generic Discrimination--Sorting and Partitioning Unshared Data in Linear Time
Fritz Henglein;
DIKU, University of Copenhagen
Session 5 (chair: Norman Ramsey)
17:00 Transactional Events for ML
Laura Effinger-Dean, Matthew Kehrt, Dan Grossman;
University of Washington
17:25 Experience Report: Erlang in Acoustic Ray Tracing
Christian Convey1, Andrew Fredricks1, Christopher Gagner1, Douglas Maxwell1, Lutz Hamel2;
1Naval Undersea Warfare Centers, RI, USA, 2Dept. of Computer Science and Statistics, University of Rhode Island
17:45 Implicitly-threaded parallelism in Manticore
Matthew Fluet1, Mike Rainey2, John Reppy2, Adam Shaw2;
1Toyota Technological Institute at Chicago, 2University of Chicago
18:10 PC chair's report
Tuesday, September 23
Invited Talk (chair: James Hook)
9:00 Defunctionalized Interpreters for Higher-Order Languages
Olivier Danvy;
University of Aarhus
Session 6 (chair: Andrew Tolmach)
10:30 Parametric Higher-Order Abstract Syntax for Mechanized Semantics
Adam Chlipala;
Harvard University
10:55 Typed Closure Conversion Preserves Observational Equivalence
Amal Ahmed and Matthias Blume;
Toyota Technological Institute at Chicago
Session 7 (chair: Manuel Chakravarty)
11:50 Write it Recursively: A Generic Framework for Optimal Path Queries
Akimasa Morihata, Kiminori Matsuzaki, Masato Takeichi;
University of Tokyo
12:15 Efficient Nondestructive Equality Checking for Trees and Graphs
Michael D. Adams and R. Kent Dybvig;
Indiana University
Session 8 (chair: Zhenjiang Hu)
14:00 Functional Pearl: Streams and Unique Fixed Points
Ralf Hinze, University of Oxford
14:25 Data-Flow Testing of Declarative Programs PPT
Sebastian Fischer1 and Herbert Kuchen2;
1University of Kiel, 2University of Münster
Session 9 (chair: Andrew Kennedy)
15:20 Functional Translation of a Calculus of Capabilities
Arthur Charguéraud and François Pottier;
INRIA
15:45 Experience Report: Paradise: A Two-Stage DSL Embedded in Haskell
Lennart Augustsson, Howard Mansell, Ganesh Sittampalam;
Credit Suisse
16:05 Ynot: Reasoning with the Awkward Squad
Aleksandar Nanevski1, Greg Morrisett2, Avi Shinnar2, Paul Govereau2, Lars Birkedal3;
1Microsoft Research, Cambridge, 2Harvard University, 3IT University, Copenhagen
Session 10 (chair: Michael Sperber)
17:00 A Scheduling Framework for General-Purpose Parallel Languages
Matthew Fluet1, Michael Rainey2, John Reppy2;
1Toyota Technological Institute at Chicago, 2University of Chicago
17:25 Space Profiling for Parallel Functional Programs
Daniel Spoonhower1, Guy E. Blelloch1, Robert Harper1, Phillip B. Gibbons2;
1Carnegie Mellon University, 2Intel Reseach Pittsburgh
Awards and Announcements (chair: Kevin Millikin)
18:00 ICFP 2009 Announcement
Phil Wadler
18:10 Most Influential ICFP'98 Paper Award
Kathleen Fisher
18:20 Report on the Eleventh ICFP Programming Contest
Tim Sheard, Tim Chevalier, Chuan-kai Lin, Garrett Morris, Emerson Murphy-Hill, Andy Gill, John Reppy, Lars Bergstrom, Mike Rainey, Adam Shaw, Virgil Gheorghiu;
Portland State University, University of Chicago
Wednesday, September 24
Invited Talk (chair: Mitchell Wand)
9:00 Polymorphism and Page Tables--Systems Programming From a Functional Programmer's Perspective
Mark Jones;
Portland State University
Session 11 (chair: Fritz Henglein)
10:30 Pattern Minimization Problems over Recursive Data Types
Alexander Krauss;
TU München
10:55 Deciding kCFA is complete for EXPTIME
David Van Horn and Harry Mairson;
Brandeis University
Session 12 (chair: Derek Dreyer)
11:50 HMF: Simple Type Inference for First-Class Polymorphism
Daan Leijen;
Microsoft Research
12:15 FPH: First-class Polymorphism for Haskell
Dimitrios Vytiniotis1, Stephanie Weirich1, Simon Peyton Jones2;
1University of Pennsylvania, 2Microsoft Research
Session 13 (chair: Chung-chieh Shan)
14:00 Mixin' Up the ML Module System
Derek Dreyer and Andreas Rossberg;
MPI-SWS
14:25 Compiling Self-Adjusting Programs with Continuations
Ruy Ley-Wild1, Matthew Fluet2, Umut Acar2;
1Carnegie Mellon University, 2Toyota Technological Institute at Chicago
Session 14 (chair: Henrik Nilsson)
15:20 Flask: Staged Functional Programming for Sensor Networks
Geoffrey Mainland, Greg Morrisett, Matt Welsh;
Harvard University
15:45 Experience Report: A Pure Shirt Fits Reflections on Haskell at Bluespec
Ravi Nanavati;
Bluespec, Inc.
16:05 Functional Netlists
Sungwoo Park, Jinha Kim, Hyeonseung Im;
Pohang University of Science and Technology
Session 15 (chair: Kathleen Fisher)
17:00 NixOS: A Purely Functional Linux Distribution
Eelco Dolstra1 and Andres Löh2;
1Delft University of Technology, 2Utrecht University
17:25 Experience Report: Visualizing Data through Functional Pipelines
David Duke1, Rita Borgo1, Colin Runciman2, Malcolm Wallace2;
1University of Leeds, UK, 2University of York, UK
17:45 Quotient Lenses
J. Nathan Foster1, Alexandre Pilkiewicz2, Benjamin C. Pierce1;
1University of Pennsylvania, 2Ecole Polytechnique
我给新来博士生的入门资料列表
我还不是博导，但是有一个搞硬件设计的08级博士生有意向跟我做这个方向，这跟我03年的情况多像。
这是我给他的入门资料列表
我拟了一个列表
逻辑方面
1 《LOGIC FOR COMPUTER SCIENCE>> 就在我拷给你的book/lcs.pdf,既然要搞这一行，那么基本的逻辑就要搞懂，看看有个概念就行
2 <>，这是对命题逻辑可解性的简单介绍
3 http://en.wikipedia.org/wiki/Boolean_satisfiability_problem 是wikipedia给出的SAT介绍
4 BDD是另一个重要的命题逻辑推理技术，这是wiki给出的介绍http://en.wikipedia.org/wiki/Binary_decision_diagram
5 另一个BDD的介绍，http://www.cse.iitd.ernet.in/~mbala/cs719/lectures/lect31/index.htm
6 BDD的经典论文，http://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.ps
7 一阶逻辑的定理证明的一本著名的书，Logic For Computer Science Foundations of Automatic Theorem Proving，就在我给你的book/ball03all.pdf，这是后继的SMT的基础
8 SMT是结合了SAT和一阶逻辑的一种推理技术，看看wikipedia的说法，http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories
9 自动机的东西就是book/lncs2500
10 高阶定理证明coq art.pdf，我这里有一个OCR的版本，来拷
编程语言，尤其是fontional programming
1 book/lambda calculus with type.pdf 是functional programming的基础
2 Practical Foundations for Programming languages，这本书讲的很全，看看，但是目前这个阶段不要强求什么都理解
软件工具
1 ocaml是一种functional 编程语言，上网去找他的完整编程环境吧。他不仅能教给你functional 的思想，本身也是一种高效的编程语言，许多形式化验证的工具都是用ocaml写的，包括大部分SMT solver， 和blast模型检测器，coq定理证明器等
2 haskell是另一种，但是太艰深了，以后再说吧
这是我给他的入门资料列表
我拟了一个列表
逻辑方面
1 《LOGIC FOR COMPUTER SCIENCE>> 就在我拷给你的book/lcs.pdf,既然要搞这一行，那么基本的逻辑就要搞懂，看看有个概念就行
2 <
3 http://en.wikipedia.org/wiki/Boolean_satisfiability_problem 是wikipedia给出的SAT介绍
4 BDD是另一个重要的命题逻辑推理技术，这是wiki给出的介绍http://en.wikipedia.org/wiki/Binary_decision_diagram
5 另一个BDD的介绍，http://www.cse.iitd.ernet.in/~mbala/cs719/lectures/lect31/index.htm
6 BDD的经典论文，http://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.ps
7 一阶逻辑的定理证明的一本著名的书，Logic For Computer Science Foundations of Automatic Theorem Proving，就在我给你的book/ball03all.pdf，这是后继的SMT的基础
8 SMT是结合了SAT和一阶逻辑的一种推理技术，看看wikipedia的说法，http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories
9 自动机的东西就是book/lncs2500
10 高阶定理证明coq art.pdf，我这里有一个OCR的版本，来拷
编程语言，尤其是fontional programming
1 book/lambda calculus with type.pdf 是functional programming的基础
2 Practical Foundations for Programming languages，这本书讲的很全，看看，但是目前这个阶段不要强求什么都理解
软件工具
1 ocaml是一种functional 编程语言，上网去找他的完整编程环境吧。他不仅能教给你functional 的思想，本身也是一种高效的编程语言，许多形式化验证的工具都是用ocaml写的，包括大部分SMT solver， 和blast模型检测器，coq定理证明器等
2 haskell是另一种，但是太艰深了，以后再说吧
2008年10月15日星期三
Essentials of Programming Languages itpub
"Essentials of Programming Languages" can be found on ITPUB, but I just lost the password.
Richard Bornat (Middlesex page)
This people do lots of research on inductive separation logic. So may interference with my data integration proof.
VMCAI 09 accepted paper and their link
- Christos Dimoulas and Mitchell Wand. The Higher-order Aggregate Update Problem
- Patrice Godefroid and Nir Piterman. LTL Generalized Model Checking Revisited
- Rotem Oshman. An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking
- Mark Kattenbelt, Marta Kwiatkowska, Gethin Norman and David Parker. Abstraction Refinement for Probabilistic Software
- Dilian Gurov and Marieke Huisman. Reducing Behavioural to Structural Properties of Programs with Procedures
- William Benton and Charles Fischer. Mostly-functional Behavior in Java Programs
- Radu Siminiceanu, Andy Galloway, Gerald Luettgen and Tobias Muehlberg. Model-Checking the Linux Virtual File System
- Michal Rutkowski, Marcin Jurdzinski and Ranko Lazic. Average-Price/Reward Games on Hybrid Automata with Strong Resets
- Johannes Kinder, Helmut Veith and Florian Zuleger. An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries
- Matthew Might and Panagiotis Manolios. A Posteriori Soundness for Non-deterministic Abstract Interpretations
- Ralf Wimmer, Bettina Braitling and Bernd Becker. Counterexample Generation for Discrete-time Markov Chains using Bounded Model Checking
- Andreas Holzer, Christian Schallhart, Michael Tautschnig and Helmut Veith. Query-Driven Program Testing
- Nicholas Kidd, Thomas Reps, Julian Dolby and Mandana Vaziri. Finding Concurrency-Related Bugs using Random Isolation
- Hasan Amjad and Richard Bornat. Towards Automatic Stability Analysis for Rely-Guarantee Proofs
- Thomas Wahl and Richard Trefler. Extending Symmetry Reduction by Exploiting System Architecture
- Vincent Laviron and Francesco Logozzo. SubPolyhedra : A (More) Scalable Approach to Infer Linear Inequalities
- Kousha Etessami and Patrice Godefroid. An Abort-Aware Model of Transactional Programming
- Viktor Vafeiadis. Shape-value Abstraction for Verifying Linearizability
- Sumit Gulwani, Saurabh Srivastava and Ramarathnam Venkatesan. Constraint-based Invariant Inference over Predicate Abstraction
- Ou Wei, Arie Gurfinkel and Marsha Chechik. Mixed Transition Systems Revisited
- Ankur Taly, Sumit Gulwani and Ashish Tiwari. Synthesizing Switching Logic using Constraint Solving
- Kalpana Gondi, Yogeshkumar Patel and A. Prasad Sistla. Monitoring the Full Range of Omega-regular Properties of Stochastic Systems
- Patrick Maier. Deciding Extensions of the Theories of Vectors and Bags
- Zvonimir Rakamaric and Alan Hu. A Scalable Memory Model for Low-Level Code
Another list of ASPDAC accepted paper
Session 8C Verification, Test, and Yield
Time: 13:30 - 15:35 Thursday, January 22, 2009
Location: Room 414+415
8C-1 (Time: 13:30 - 13:55)
8C-2 (Time: 13:55 - 14:20)
8C-3 (Time: 14:20 - 14:45)
8C-4 (Time: 14:45 - 15:10)
8C-5 (Time: 15:10 - 15:35)
Time: 13:30 - 15:35 Thursday, January 22, 2009
Location: Room 414+415
8C-1 (Time: 13:30 - 13:55)
| Title | Self-Adjusting Constrained Random Stimulus Generation Using Splitting Evenness Evaluation and XOR Constraints |
| Author | Shujun Deng, Zhiqiu Kong, Jinian Bian, Yanni Zhao (Department of Computer Science and Technology, Tsinghua University, China) |
| Keyword | stimulus generation, SAT, even distribution, splitting, XOR constraint |
| Abstract | A linear dynamic method to guide random stimulus generation by SAT solvers is presented. Firstly, we analyze different evenness evaluation methods. Secondly, we applied split simplified Min-Distance-Sum evaluation methods and XOR sampling to fulfill self-adjusting random stimulus generation. Experimental results show that our method can evaluate the evenness as well as more complex formulae for stimulus generation, and also confirm that the dynamic evaluation combining with XOR sampling can improve the power of constrained simulation. |
| Title | Diagnosing Integrator Leakage of Single-Bit First-Order Delta-Sigma Modulator Using DC Input |
| Author | Xuan-Lun Huang, Chen-Yuan Yang, Jiun-Lang Huang (Graduate Institute of Electronics Engineering, Department of Electrical Engineering, National Taiwan University, Taiwan) |
| Keyword | analog/mixed-signal testing, diagnosis, design-for-test (DfT), delta-sigma modulation, integrator leakage |
| Abstract | Integrator leakage is a dominant factor in the SNR (signal-to-noise ratio) loss of delta-sigma modulators. In this paper, we propose a Design-for-Test (DfT) technique to diagnose the integrator leakage of the single-bit first-order delta-sigma modulator. The proposed technique is a low-cost solution; it only adds two multiplexers to the modulator, utilizes a single DC voltage as the test stimulus, and estimates the integrator leakage by analyzing the digitized bit stream. Furthermore, the technique can be easily extended to higher order delta-sigma modulators. Simulation results show that accurate estimations of the integrator leakage can be achieved even at the presence of noise. |
| Title | Path Selection for Monitoring Unexpected Systematic Timing Effects |
| Author | Nicholas Callegari, Pouria Bastani, Li-C. Wang (University of California, Santa Barbara, United States), Sreejit Chakravarty, Alex Tetelbaum (LSI Corp., United States) |
| Keyword | clustering, path delay, path selection, delay test |
| Abstract | This paper presents a novel path selection methodology to select paths for monitoring unexpected systematic timing effects. The methodology consists of three components: path filtering, path encoding, and path clustering. Given a large set of critical paths, in path filtering, the goal is to filter out paths that cannot be functionally sensitized. To explore the space of unexpected timing effects, a set of features are defined to encode paths into path vectors. Each feature is a source of concern that may potentially contribute to the cause of an unexpected timing effect. Finally, a kernel-based clustering algorithm is employed to group similar path vectors into clusters from which the best representative paths are selected for post-silicon monitoring. The effectiveness of our proposed methodology is demonstrated through experiments on an industrial ASIC design. |
| Title | Design for Burn-In Test: A Technique for Burn-In Thermal Stability under Die-to-Die Parameter Variations |
| Author | Mesut Meterelliyoz, Kaushik Roy (Purdue University, United States) |
| Keyword | burn-in, leakage, thermal, stability, variations |
| Abstract | Strong temperature dependence of leakage has been a major problem during burn-in test where increased voltages and temperatures are applied to weed out defective parts. Moreover, process variations may result in different temperature profiles in different dies during burn-in. This paper proposes an adaptive design-for-burn-in technique that stabilizes the junction temperature by controlling the leakage power using sleep transistors for a wide range of ambient temperatures, process variations, thermal resistances and supply voltages. |
| Title | Test Infrastructure Design for Core-Based System-on-Chip Under Cycle-Accurate Thermal Constraints |
| Author | Thomas Edison Yu, Tomokazu Yoneda (Nara Institute of Science and Technology, Japan), Krishnendu Chakrabarty (Duke University, United States), Hideo Fujiwara (Nara Institute of Science and Technology, Japan) |
| Keyword | SoC test, TAM design, test scheduling, thermal-aware test, wrapper design |
| Abstract | We present a thermal-aware test-access mechanism (TAM) design and test scheduling method for system-on-chip integrated circuits. The proposed method uses cycle-accurate power profiles for thermal simulation; it also relies on test-set partitioning, test-interleaving, and bandwidth matching. We use a computationally tractable thermal-cost model to ensure that temperature constraints are satisfied and the test application time is minimized. Simulation results for the ITC’02 SOC Test Benchmarks show that, compared to prior thermal-aware test-scheduling techniques, the proposed method leads to shorter test times under tight temperature constraints. |
ASPDAC 09 accepted paper and their link
Session 7B Sequential Design Verification
Time: 10:15 - 12:20 Thursday, January 22, 2009
Location: Room 413
7B-1 (Time: 10:15 - 10:40)
7B-2 (Time: 10:40 - 11:05)
7B-3 (Time: 11:05 - 11:30)
7B-4 (Time: 11:30 - 11:55)
7B-5 (Time: 11:55 - 12:20)
Time: 10:15 - 12:20 Thursday, January 22, 2009
Location: Room 413
7B-1 (Time: 10:15 - 10:40)
| Title | Dependent Latch Identification in the Reachable State Space |
| Author | Chen-Hsuan Lin, Chun-Yao Wang (National Tsing Hua University, Taiwan) |
| Keyword | dependent latch, functional dependency, reachability analysis |
| Abstract | The large number of latches in current designs increase the complexity of formal verification and logic synthesis. The reason for this is that the growth of latch number leads the state space to explode exponentially. One solution to this problem is to find the functional dependencies among these latches. With the identification of functional dependencies, these latches can be identified as dependent latches or essential latches, where the state space can be constructed using only the essential latches. Although much research has been devoted to exploring the functional dependencies among latches by BDD-based symbolic algorithms, this issue is still unresolved for large sequential circuits. In this work, we find the functional dependencies among latches in a sequential circuit by using SAT solvers with the Craig interpolation theorem. In addition, our proposed approach detects sequential functional dependencies existing in the reachable state space only. The sequential functional dependencies can identify additional dependent latches after a specific timeframe in order to achieve additional reduction of the state space. Experimental results show that this approach could deal with large sequential circuits with up to 1.5K latches in a reasonable time and simultaneously identify the combinational and sequential dependent latches. |
| Title | Complete-k-Distinguishability for Retiming and Resynthesis Equivalence Checking without Restricting Synthesis |
| Author | Nikolaos Liveris, Hai Zhou (Northwestern University, United States), Prithviraj Banerjee (HP Labs, United States) |
| Keyword | sequential equivalence checking, retiming and resynthesis, verification |
| Abstract | Performing retiming and resynthesis iteratively is a powerful way to optimize sequential circuits. In this paper we tackle the problem of verifying the equivalence of a pair of circuits, one of which has been obtained from the other by a sequence of retiming and resynthesis operations. For this purpose we extend the Complete-1-Distinguishability (C-1-D) property to C-$k$-D for any natural $k$. We show how we can simplify the equivalence checking problem, if one of the circuits satisfies this property. Our method for checking equivalence is complete for any number of retiming and resynthesis steps. Moreover, we show a way to enforce C-$k$-D to one of the circuits without restricting the optimization power of retiming and resynthesis or increasing their complexity. Our experimental results show that by enforcing the C-$k$-D property we can speed up the verification process. |
| Title | Disjunctive Transition Relation Decompositions for Multithreaded Image Computation |
| Author | Stergios Stergiou, Jawahar Jain (Fujitsu Laboratories of America, United States) |
| Keyword | formal verification, model checking, disjunctive decomposition |
| Abstract | We investigate disjunctive Transition Relation decompositions in the context of multi-threaded symbolic model checking. We propose an algorithm that generates such decompositions and an adaptive image computation algorithm which efficiently exploits the multi-threaded platform. We integrated the algorithms in VIS and tested them on the VIS benchmarks. We show that the obtained decompositions are well-balanced and the algorithm compares favorably with more traditional conjunctive image computation approaches. |
| Title | Multi-Clock SVA Synthesis without Re-writing |
| Author | Jiang Long, Andrew Seawright, Paparao Kavalipati (Mentor Graphics Corp., United States) |
| Keyword | SVA, Formal verification, Multi-Clock |
| Abstract | This paper presents a compilation procedure for synthesiz- ing multi-clock SVA properties for formal verification. The synthesis framework is built upon an existing compilation al- gorithm for single-clock SVA properties. While we could use the SVA rewriting rules to transform a multi-clock property into a single-clocked property and then apply existing tech- niques, instead we propose techniques to selectively model the multi-clock operators to produce a smaller checker logic. Through recursive construction and syntactic transforma- tion, we are able demonstrate the efficiency of the technique and the generated checker logic is provably equivalent to the rewriting version. |
| Title | Automatic Formal Verification of Clock Domain Crossing Signals |
| Author | Bing Li, Chris Kwok (Mentor Graphics Corporation, United States) |
| Keyword | formal verification, clock domain crossing, assertion logic |
| Abstract | In this paper, we present an approach that uses formal methods to verify Clock Domain Crossing (CDC) issues in a fully automatic way. First, we discuss various CDC schemes and the corresponding checks that need to be formally verified. Then we demonstrate how to synthesize them into assertion logic. After that a fully automatic, on-the-fly formal CDC approach is proposed. To the best of our knowledge, this is the first paper discussing fully automatic, on-the-fly formal verification of CDC signals. Experiment results show that our automatic formal CDC, when compared with the conventional post-CDC formal CDC, takes much less time, but still prove significant number of CDC checks. |
POPL 09 accepted papers and their link
Automatic modular abstractions for linear constraints
David Monniaux, CNRS / VERIMAG
Static Contract Checking for Haskell ppt
Dana N. Xu, University of Cambridge,
Simon Peyton Jones, Microsoft Research
Koen Claessen, Chalmers University of Technology
Proving that non-blocking algorithms don't block ppt
Alexey Gotsman, University of Cambridge
Byron Cook, Microsoft Research
Matthew Parkinson, University of Cambridge
Viktor Vafeiadis, Microsoft Research
Types and Higher-Order Recursion Schemes for Verification of Higher-Order Programs
Naoki Kobayashi, Tohoku University
Compositional Shape Analysis
Cristiano Calcagno, Imperial College, London
Dino Distefano, Queen Mary, University of London
Peter O'Hearn, Queen Mary, University of London
Hongseok Yang, Queen Mary, University of London
Semi-Sparse Flow-Sensitive Pointer Analysis
Ben Hardekopf, The University of Texas at Austin
Calvin Lin, The University of Texas at Austin
Feedback-Directed Barrier Optimization in a Strongly Isolated STM
Nathan Bronson, Stanford CS
Christos Kozyrakis, Stanford CS
Kunle Olukotun, Stanford CS
Modular Code Generation from Synchronous Block Diagrams: Modularity vs. Code Size
Roberto Lublinerman, The Pennsylvania State University
Christian Szegedy, Cadence Research Laboratories
Stavros Tripakis, Cadence Research Laboratories
Formal Certification of Code-Based Cryptographic Proofs
Gilles Barthe, IMDEA Software, Madrid and Microsoft Research - INRIA Joint Centre
Benjamin Gregoire, INRIA Sophia Antipolis and Microsoft Research - INRIA Joint Centre
Santiago Zanella, INRIA Sophia Antipolis and Microsoft Research - INRIA Joint Centre
Relaxed memory models: an operational approach
Gerard Boudol, INRIA Sophia Antipolis
Gustavo Petri, INRIA Sophia Antipolis
Bidirectionalization for Free! (Pearl)
Janis Voigtlander, Technische Universitat Dresden
The Semantics of x86 Multiprocessor Machine Code
Susmit Sarkar, University of Cambridge
Peter Sewell, University of Cambridge
Francesco Zappa Nardelli, INRIA
Scott Owens, University of Cambridge
Thomas Braibant, INRIA
Magnus Myreen, University of Cambridge
Jade Alglave, INRIA
Flexible types: Robust type inference for first-class polymorphism
Daan Leijen, Microsoft Research
Verifying Liveness for Asynchronous Programs
Pierre Ganty, UC Los Angeles
Rupak Majumdar, UC Los Angeles
Andrey Rybalchenko, MPI SWS
Masked types for sound object initialization
Xin Qi, Cornell University
Andrew C. Myers, Cornell University
A Model of Cooperative Threads
Martin Abadi, Microsoft and UCSC
Gordon Plotkin, University of Edinburgh and Microsoft
State-Dependent Representation Independence
Amal Ahmed, TTI-C
Derek Dreyer, MPI-SWS
Andreas Rossberg, MPI-SWS
Equality Saturation: a new Approach to Optimization
Ross Tate, UC San Diego
Michael Stepp, UC San Diego
Zachary Tatlock, UC San Diego
Sorin Lerner, UC San Diego
The Semantics of Progress in Lock-Based Transactional Memory
Rachid Guerraoui, EPFL
Michal Kapalka, EPFL
Positive Supercompilation for a higher order call-by-value language
Peter A. Jonsson, Lulea University of Technology
Johan Nordlander, Lulea University of Technology
Unifying Type Checking and Property Checking for Low-Level Code
Jeremy Condit, Microsoft Research
Brian Hackett, Stanford University
Shuvendu Lahiri, Microsoft Research
Shaz Qadeer, Microsoft Research
The Third Homomorphism Theorem on Trees: Downward & Upward Lead to Divide-and-Conquer
Akimasa Morihata, University of Tokyo
Kiminori Matsuzaki, University of Tokyo
Zhenjiang Hu, National Institute of Informatics
Masato Takeichi, University of Tokyo
On verifying enterprise infrastructure
Tom Ridge, University of Cambridge
A Foundation for Flow-Based Program Matching Using Temporal Logic and Model Checking
Julien Brunel, DIKU, University of Copenhagen
Damien Doligez, INRIA, Gallium Project
Rene Rydhof Hansen, Aalborg University
Julia L. Lawall, DIKU, University of Copenhagen
Gilles Muller, Ecole des Mines de Nantes
A Calculus of Atomic Actions
Tayfun Elmas, Koc University
Shaz Qadeer, Microsoft Research
Serdar Tasiran, Koc University
Copy-on-Write in the PHP Language
Akihiko Tozawa, IBM Tokyo Research Lab.
Michiaki Tatsubori, IBM Tokyo Research Lab.
Tamiya Onodera, IBM Tokyo Research Lab.
Yasuhiko Minamide, Tsukuba University
Local Rely-Guarantee Reasoning
Xinyu Feng, Toyota Technological Institute at Chicago
Classical BI (A Logic for Reasoning about Dualising Resource)
James Brotherston, Imperial College London
Cristiano Calcagno, Imperial College London
Why are open existential types are so good?
Benoit Montagu, INRIA
Didier Remy, INRIA
Lazy Evaluation and Delimited Control
Ronald Garcia, Indiana University
Andrew Lumsdaine, Indiana University
Amr Sabry, Indiana University
Automated Verification of Practical Garbage Collectors
Chris Hawblitzel, Microsoft Research
Erez Petrank, Microsoft Research
A Combination Framework for Tracking Partition Sizes
Sumit Gulwani, Microsoft Research
Tal Lev-Ami, Tel-Aviv University
Mooly Sagiv, Tel-Aviv University
The Theory of Deadlock Avoidance via Discrete Control
Yin Wang, Discrete Event Systems Lab, U. Michigan EECS
Scott Mahlke, Advanced Computer Architecture Lab, U. Michigan EECS
Stephane Lafortune, Discrete Event Systems Lab, U. Michigan EECS
Terence Kelly, HP Labs
Manjunath Kudlur, Advanced Computer Architecture Lab, U. Michigan EECS
SPEED: Precise and Efficient Static Estimation of Program Computational Complexity
Sumit Gulwani, Microsoft Research
Krishna Mehra, Microsoft Research
Trishul Chilimbi, Microsoft Research
A Cost Semantics for Self-Adjusting Computation
Ruy Ley Wild, Carnegie Mellon University
Umut A. Acar, Toyota Technological Institute
Matthew Fluet, Toyota Technological Institute
Focusing on Pattern Matching
Neelakantan Krishnaswami, Carnegie Mellon University
Upcoming conf
ASPDAC 09 08/Aug
ICSE 09 08/Aug/29
POPL 09 08/Jul/08
ASPLOS 09 08/Aug/01
VMCAI 09 08/Aug/26
DATE 09 08/Sep/07
TACAS 09 08/Oct/02
HSCC 09 08/Oct/17
PLDI 09 08/Nov/02
DAC 09 08/Dec/19
LICS 09 09/Jan/12
CAV 09 09/Jan/18
SIGCOMM 09 09/Jan/23
SAS 09 09/Feb/10
SAT 09 09/Feb/20
CADE 09 09/Feb/16
ICFP 09 09/March/02
SPIN 09 09/March/09
FSE 09 09/March/16
ATVA 09 09/May/01
FM 09 09/May/04
ASE 09
CONCUR 09
FMCAD 09
ICCAD 09
ICSE 09 08/Aug/29
POPL 09 08/Jul/08
ASPLOS 09 08/Aug/01
VMCAI 09 08/Aug/26
DATE 09 08/Sep/07
TACAS 09 08/Oct/02
HSCC 09 08/Oct/17
PLDI 09 08/Nov/02
DAC 09 08/Dec/19
LICS 09 09/Jan/12
CAV 09 09/Jan/18
SIGCOMM 09 09/Jan/23
SAS 09 09/Feb/10
SAT 09 09/Feb/20
CADE 09 09/Feb/16
ICFP 09 09/March/02
SPIN 09 09/March/09
FSE 09 09/March/16
ATVA 09 09/May/01
FM 09 09/May/04
ASE 09
CONCUR 09
FMCAD 09
ICCAD 09
from data to structrue
Nowadays programming jobs rely on data structure-- so many library and packages, contain so many data structure definitions, what a pain to learn all of these !!!
Generally,we often has some insight in how the data should be arranged, for example, if we are using a java package iText to parse pdf, and want to extract a table from it, then we should know there are some text that should appear at the same sub level under some data structure.
So if the language support query with 2D RE, then we can find out this data structure.
This feature is very useful in script language such as JS and TCL.
And furthermore, we may develop a brand new programming approach that access data by its pattern, instead of following data structure explictly. The compiler should scan the data structure to fill in the missed detail, in a way that is somewhat similar to type inference and sketch programming.
Current problem is : if this idea has been invented by ASPECT-programming or new generation of functional language such as Agda?
Generally,we often has some insight in how the data should be arranged, for example, if we are using a java package iText to parse pdf, and want to extract a table from it, then we should know there are some text that should appear at the same sub level under some data structure.
So if the language support query with 2D RE, then we can find out this data structure.
This feature is very useful in script language such as JS and TCL.
And furthermore, we may develop a brand new programming approach that access data by its pattern, instead of following data structure explictly. The compiler should scan the data structure to fill in the missed detail, in a way that is somewhat similar to type inference and sketch programming.
Current problem is : if this idea has been invented by ASPECT-programming or new generation of functional language such as Agda?
Typed assembly language
Typed assembly language incorporate typeness into assembly language .
It seems a viable approach to prevent security problem.
But it can only check program that contain source code. what if we download binary from internet?
There are some people doing researching on reasoning binary code.such as PCC(proof carrying code)
Can we incorporate type checking into CPU design?
Can we enforce seperation logic semantics by water print on pointer?
It seems a viable approach to prevent security problem.
But it can only check program that contain source code. what if we download binary from internet?
There are some people doing researching on reasoning binary code.such as PCC(proof carrying code)
Can we incorporate type checking into CPU design?
Can we enforce seperation logic semantics by water print on pointer?
A very light weight VM at application level and can be started/cloned in place
existing VM are all need to start up some wrapper environment to seperate guest OS/app from each other, to achive security.
But some time I dont need such full scale mechnism, I only need to seperate different running of application.
For example, I need to install formality that need some old system wide setting and old libray , and I dont want these setting to affect others,I dont want to do any special setting, I just want to
But some time I dont need such full scale mechnism, I only need to seperate different running of application.
For example, I need to install formality that need some old system wide setting and old libray , and I dont want these setting to affect others,I dont want to do any special setting, I just want to
- firstly make a clone of existing setting ,this step need to be very cheap
- and do all change on this clone, such as install app, and related lib
- I can chose to merge it into origin environment.
protect OS itself from affected
All state of the art virtual machines try to seperate guest OSs from each other. If one die, other will not be affected.
But what if we has place important data in that dead guest OS? what if we has put lots of human hours to install and config this golden OS, and it has already cumulate valueable information on his long run?
For example, I install bank USB-key driver on my winXP in vmware, which is very hard to reinstall, and the outlook also record all my contact, mail, calendar,all these are very valuable. just deleting the VM will lost all these things.
So I think we still need to protect individual OS from attack, even if we has virtual machine.
On the other hand, DRAM price is so low these days,I can easiely install 6G memory to may dell desktop PC. But running all my every day program only need 512MB.
So if this means that we can sacrify 10 times of memory to exchange for security?
The tagged memory approach may seem an idea to be further refined.
But what if we has place important data in that dead guest OS? what if we has put lots of human hours to install and config this golden OS, and it has already cumulate valueable information on his long run?
For example, I install bank USB-key driver on my winXP in vmware, which is very hard to reinstall, and the outlook also record all my contact, mail, calendar,all these are very valuable. just deleting the VM will lost all these things.
So I think we still need to protect individual OS from attack, even if we has virtual machine.
On the other hand, DRAM price is so low these days,I can easiely install 6G memory to may dell desktop PC. But running all my every day program only need 512MB.
So if this means that we can sacrify 10 times of memory to exchange for security?
The tagged memory approach may seem an idea to be further refined.
Guide to the history of web application framwork
This wiki page give guide on the history of web application framework, at the bottom of that page, list the comparation between state of the art frameworks
It seems that PHP on server side + Javascript on client side is very popular.
So reasoning across JS and PHP seems cool.
It seems that PHP on server side + Javascript on client side is very popular.
So reasoning across JS and PHP seems cool.
2008年10月14日星期二
Using library without reading documentation??
what a pain to understand the looooooong documentation before using the desired libraries. There are so many data structrue and function definition, to get one thing, I must follow a pointer with argly name,to get another thing, I must call a strange function.
So can we avoid this??
And we dont want to put extra burdent on library developer to support this.
So I think we may need to do a transitive closure computing to find out all ways of geting to other object, by following pointer and/or calling functions.
Problem of this way is that, we may get huge size of data. But we can overcome this by lazy evluation of haskell.
On the other hand, Maybe my previous idea on general data structrue enumerator is a partial solution to this.
By general data structrue enumerator, I means that we only need to call a special function or invoke a special syntax, and give out the condition expressed in regular expression(or 2D RE for tree like structure?), then give the statement to be executed.
So can we avoid this??
And we dont want to put extra burdent on library developer to support this.
So I think we may need to do a transitive closure computing to find out all ways of geting to other object, by following pointer and/or calling functions.
Problem of this way is that, we may get huge size of data. But we can overcome this by lazy evluation of haskell.
On the other hand, Maybe my previous idea on general data structrue enumerator is a partial solution to this.
By general data structrue enumerator, I means that we only need to call a special function or invoke a special syntax, and give out the condition expressed in regular expression(or 2D RE for tree like structure?), then give the statement to be executed.
OSDI 08 : Hardware Enforcement of Application Security Policies Using Tagged Memory
This paper use tagged mamory to enforce security
What a pitty, this idea pop out my head 1 and a half years before, But I just dont has that time to follow up it.
What a pitty, this idea pop out my head 1 and a half years before, But I just dont has that time to follow up it.
OSDI 08 : Difference Engine: Harnessing Memory Redundancy in Virtual Machines
This paper try to share VM content at sub page level, instead of the traditional page level. the use patch to represent the difference between them
OSDI 08: CuriOS: Improving Reliability through Operating System Structure
This paper solve the traditional problem that, when restart a service in OS, if that service is maintaining state of some client(such as the opened file handler), then restart will lost these information.
The main idea is to seperate the state of client from server into a standalone space, that are belong to neither server or client. the server only access these state when he receive some request from corresponding client.
Then if we reset the server, these state still remain there.
OSDI'08 : Corey: an operating system for many cores
main idea of this paper is to expose low level detail to up level software, much like exokernel, HAHA, Dawson Angle jump out agiain.
U Rank:collaborating searching
MSR again bring us an interesting topic:U rank, which can make your searching history and searching result be shared to others , who also interest in this .
订阅：
博文 (Atom)
博文
