VMCAI09: Mostly-Functional Behavior in Java Programs

it propose a type and effect system that can find out "run time constance" variables in JAVA.

I remember that I read a related paper a couple of  months before, that paper discuss "stationary" field, which is similar to to this.

similar mechnism include the java standard "final" field, which is some what too restricted.

So in summary, there are three class of such mechnism:

final,too strong

stationary

quie scing

Such mechnism can prevent those variables from been initialied or writen more than one time.typical application include OO system that need to initite newlly allocated object.

Its slide describe an interesting relation between type system and effect system, the formmer one describe "what is the object",while the later one describe "how the object behave"

tacas 09 accepted papers

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

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?

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

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?