Nadeem Iqbal | 5 Feb 04:42 2016
Picon

About Binary Relations

Hi,

Dear All,

I am working in HOL4. I want to extract the domain of the set of binary relations.
For example, when I tried this goal,

g `! S. (FST (S CROSS S)) SUBSET (FST (S CROSS S))`;

It could not run. Can any one guide me?

Regards,

Nadeem Iqbal
HoD School of Computing and Information Sciences,
Imperial College of Business Studies,
Lahore, Pakistan.

------------------------------------------------------------------------------
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Adnan Rashid | 28 Jan 10:53 2016
Picon

About proof of an integral theorem

Dear all,

I am working in HOL Light and I want to prove the following theorem regarding integral:

!b. f absolutely_integrable_on interval [lift a,lift b]
     ==> (?k. ((\b. real_integral (real_interval [a,b]) (\t. norm (f (lift t)))) - - -> k) at_posinfinity)

which says that if a function is absolutely integrable on [a, infinity), i.e., the norm of function f is convergent then integral of fucntion's norm over the same interval approaches to some limit value k which is actually true.

Can anyone guide me in its proof?

Thanks.


Adnan Rashid
PhD Candidate,
NUST-SEECS,
Islamabad, Pakistan
------------------------------------------------------------------------------
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=267308311&iu=/4140
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Havelund, Klaus (349F | 27 Jan 07:26 2016
Picon
Picon

[fm-announcements] NFM 2016 - third call for papers


NFM 2016 - Call For Papers

The 8th NASA Formal Methods Symposium

http://crisys.cs.umn.edu/nfm2016

June 07 - June 09 2016


McNamara Alumni Center   
University of Minnesota   
200 Oak Street S.E., Minneapolis, MN 55455   


THEME OF THE SYMPOSIUM

The widespread use and increasing complexity of mission-critical and 
safety-critical systems at NASA and the aerospace industry requires advanced 
techniques that address their specification, design, verification, validation, 
and certification requirements. The NASA Formal Methods Symposium is a forum 
to foster collaboration between theoreticians and practitioners from NASA, 
academia, and the industry, with the goal of identifying challenges and 
providing solutions towards achieving assurance for such critical systems. 

New developments and emerging applications like autonomous on-board software 
for Unmanned Aerial Systems (UAS), UAS Traffic Management (UTM), advanced 
separation assurance algorithms for aircraft, and the need for system-wide 
fault detection, diagnosis, and prognostics provide new challenges for system 
specification, development, and verification approaches. Similar challenges 
need to be addressed during development and deployment of on-board software 
for spacecraft ranging from small and inexpensive CubeSat systems to manned 
spacecraft like Orion, as well as for ground systems.

The focus of the symposium will be on formal techniques and other approaches 
for software assurance, their theory, current capabilities and limitations, 
as well as their potential application to aerospace, robotics, and other 
NASA-relevant safety-critical systems during all stages of the software 
life-cycle. 


TOPICS OF INTEREST INCLUDE BUT ARE NOT LIMITED TO

* Model checking
* Theorem proving
* SAT and SMT solving
* Symbolic execution
* Static analysis
* Model-based development
* Runtime verification
* Software and system testing
* Safety assurance
* Fault tolerance
* Compositional verification
* Security and intrusion detection
* Design for verification and correct-by-design techniques
* Techniques for scaling formal methods
* Applications of formal methods in the development of:
    * autonomous systems
    * safety-critical artificial intelligence systems
    * cyber-physical, embedded, and hybrid systems
    * fault-detection, diagnostics, and prognostics systems
* Use of formal methods in:
    * assurance cases
    * human-machine interaction analysis
    * requirements generation, specification, and validation
    * automated testing and verification


IMPORTANT DATES

- Paper Submission:    2/19/2016
- Paper Notifications: 4/8/2016
- Camera-ready Papers: 4/27/2016
- Symposium:           6/7 - 6/9/2016


LOCATION

The symposium will take place at McNamara Alumni Center, University of Minnesota.


Registration is required but is free of charge.


SUBMISSION DETAILS

There are two categories of submissions:

1. Regular papers describing fully developed work and complete
   results (maximum 15 pages)
2. Short papers on tools, experience reports, or work in progress 
   with preliminary results (maximum 6 pages)

All papers must be in English and describe original work that has not been 
published or submitted elsewhere. All submissions will be fully reviewed by 
at least three members of the Program Committee.

Papers will appear in a volume of Springer's Lecture Notes in Computer Science 
(LNCS), and must use LNCS style formatting. Papers must be submitted in PDF 
format at the EasyChair submission site:

https://easychair.org/conferences/?conf=nfm2016

Authors of selected best papers may be invited to submit an extended
version to a special issue of the Journal of Automated Reasoning (Springer).

ORGANIZING COMMITTEE

- Michael Lowry, NASA Ames Research Center, USA (NASA Liaison)
- Johann Schumann, SGT, Inc./NASA Ames Research Center, USA (General Chair)
- Oksana Tkachuk, SGT, Inc./NASA Ames Research Center, USA (PC Chair)
- Sanjai Rayadurgam, University of Minnesota, USA (PC Chair)
- Mike Whalen, University of Minnesota, USA (Financial Chair)
- Mats Heimdahl, University of Minnesota, USA (Local Arrangements Chair)


PROGRAM COMMITTEE

- Julia Badger, NASA Johnson Space Center, USA
- Clark Barrett, New York University, USA
- Saddek Bensalem, Verimag and  University Joseph Fourier, France
- Dirk Beyer, University of Passau, Germany
- Borzoo Bonakdarpour, McMaster University, Canada
- Alessandro Cimatti, FBK, Italy
- Darren Cofer, Rockwell Collins, Inc., USA
- Myra Cohen, University of Nebraska-Lincoln, USA
- Misty Davies, NASA Ames Research Center, USA
- Leonardo de Moura, Microsoft, USA
- Ben Di Vito, NASA Langley Research Center, USA
- Alexandre Duret-Lutz, LRDE / EPITA, France
- Andrew Gacek, Rockwell Collins, Inc., USA
- Pierre-Loic Garoche, ONERA, France
- Shalini Ghosh, SRI International, USA
- Susanne Graf, Universite Joseph Fourier / CNRS / VERIMAG, France
- Radu Grosu, Stony Brook University, USA
- Arie Gurfinkel,SEI, Carnegie Mellon University, USA
- Klaus Havelund, NASA Jet Propulsion Laboratory, USA
- Constance Heitmeyer, Naval Research Laboratory, USA
- Gerard Holzmann, NASA Jet Propulsion Laboratory, USA
- Falk Howar, TU Clausthal / IPSSE, Germany
- Rajeev Joshi, NASA Jet Propulsion Laboratory, USA
- Dejan Jovanović, SRI International, USA
- Gerwin Klein, NICTA and University of New South Wales, Australia
- Daniel Kroening, University of Oxford, UK
- Rahul Kumar, NASA Jet Propulsion Laboratory, USA
- Michael Lowry, NASA Ames Research Center, USA
- Célia Martinie, ICS-IRIT, Université Paul Sabatier, France
- Eric Mercer, Brigham Young University, USA
- Cesar Munoz, NASA Langley Research Center, USA
- Jorge A Navas, SGT, Inc./NASA Ames Research Center, USA
- Natasha Neogi, NASA Langley Research Center, USA
- Ganesh Pai, SGT, Inc./NASA Ames Research Center, USA
- Charles Pecheur, Université catholique de Louvain, Belgium
- Lee Pike, Galois, Inc., USA
- Andreas Podelski, University of Freiburg, Germany
- Pavithra Prabhakar, Kansas State University, USA
- Venkatesh Prasad Ranganath, Kansas State University, USA
- Franco Raimondi, Middlesex University, UK
- Kristin Yvonne Rozier, University of Cincinnati, USA
- Neha Rungta, SGT, Inc./NASA Ames Research Center, USA
- Oleg Sokolsky, University of Pennsylvania, USA
- Stefano Tonetta, FBK, Italy
- Helmut Veith, Vienna University of Technology, Austria
- Willem Visser, Stellenbosch University, South Africa
- Virginie Wiels, ONERA / DTIM, France
- Guowei Yang, Texas State University, USA


STEERING COMMITTEE

- Julia Badger, NASA Johnson Space Center, USA 
- Ben Di Vito, NASA Langley Research Center, USA 
- Klaus Havelund, NASA Jet Propulsion Laboratory, USA
- Gerard Holzmann, NASA Jet Propulsion Laboratory, USA
- Michael Lowry, NASA Ames Research Center, USA
- Kristin Yvonne Rozier, University of Cincinnati, USA
- Johann Schumann, SGT, Inc./NASA Ames Research Center, USA

---
To opt-out from this mailing list, send an email to

fm-announcements-request <at> lists.nasa.gov

with the word 'unsubscribe' as subject or in the body. You can also make the request by contacting

fm-announcements-owner <at> lists.nasa.gov 
------------------------------------------------------------------------------
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=267308311&iu=/4140
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Ken Kubota | 26 Jan 15:27 2016
Picon

Goedel's paradox, canonical definitions vs. instances/models (dependent type theory and the language of species), expressiveness vs. automation, re-evaluating natural deduction

Dear Members of the Research Community,

Considering the results of Shinichi Mochizuki (see section 2 below) at
	http://www.kurims.kyoto-u.ac.jp/~motizuki/Inter-universal%20Teichmuller%20Theory%20IV.pdf

as well as offering a further response to Ramana Kumar's comment (see section 3 
below) at
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00149.html

and answering Andrei Popescu's comment (see section 4 below) at
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-December/msg00059.html

is a good opportunity to re-evaluate natural deduction, and to summarize and 
conclude the discussion.

Most of the statements about the Isabelle proof assistant software should also 
apply to the HOL and the Coq proof assistants.

1. Goedel's paradox (Goedel's First Incompleteness Theorem)

As shown previously at
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-January/msg00029.html
because of the non-definability of a Goedel numbering (or encoding) function 
within Q0 (or more precisely: the non-expressibility, since it is not a 
well-formed formula) due to the violation of type restrictions on lambda 
application (case (b) in the definition of wffs (well-formed formulae) [cf. 
Andrews, 2002, p. 211]), Goedel's First Incompleteness Theorem is not a 
mathematical theorem (or metatheorem), and the same is also true of Goedel's 
Second Incompleteness Theorem, since both theorems would require a wff 
representing the Goedel numbering (or encoding) function.

This violation of type restrictions in formal logic or mathematics corresponds 
to the philosophical insight that Goedel's construction of a proposition 
involving self-referencing negativity ("I am not provable") has to be 
considered as an antinomy, as both Russell's paradox ("the set of all sets that 
are not members of themselves") and Goedel's paradox known as the proposition 
in Goedel's First Incompleteness Theorem ("I am not provable", or originally: 
"We therefore have before us a proposition that says about itself that it is 
not provable" [Gödel, 1931, p. 598]) have the two constitutive properties of 
antinomies: self-reference and negativity (negation).

In the presentation of Goedel's First Incompleteness Theorem with the Isabelle 
proof assistant software, the definition of the Goedel encoding function was 
obtained by using the metamathematical notion "term" (level 1) as a concrete 
mathematical type symbol (level 2) [cf. Andrews, 2002, p. 210], which is a 
confusion of two different logical levels (or language levels), and hence a 
violation of type restrictions.

Generally speaking, due to certain decisions in the design of Isabelle the 
stratification of the three different logical levels (as, for example, in the 
R0 implementation) collapse into a single one, which requires justification and 
certain measures to prevent the confusion of logical levels (or language 
levels) within the single sphere obtained.

2. Canonical definitions vs. instances/models (dependent type theory and the 
language of species)

In his development of a "language of species", in which a "'species' is a 'type 
of mathematical object', such as a 'group', a 'ring', a 'scheme', etc." 
[Mochizuki, 2015, p. 66], one of Professor Mochizuki's interests is to 
distinguish canonical definitions from arbitrary choices: "The fact that the 
data involved in a species is given by abstract set-theoretic formulas imparts 
a certain canonicality to the mathematical notion constituted by the species, a 
canonicality that is not shared, for instance, by mathematical objects whose 
construction depends on an invocation of the axiom of choice in some particular 
ZFC-model [...]. Moreover, by furnishing a stock of such 'canonical notions', 
the theory of species allows one, in effect, to compute the extent of deviation 
of various 'non-canonical objects' [i.e., whose construction depends upon the 
invocation of the axiom of choice!] from a sort of 'canonical norm'." 
[Mochizuki, 2015, p. 70]

This is also one of the motivations for dependent type theory, in which the 
same can be expressed even more elegantly. The creator of R0 initially intended 
to prove that the definition of natural numbers by John von Neumann is a 
specific instance (model) of the canonical definition with the Peano axioms. 
For practical reasons, a simpler, but conceptually equivalent proof was carried 
out: The group property of the exclusive disjunction (XOR), which in dependent 
type theory can be directly expressed by the theorem
	Grp o XOR
as proven at
	http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf (p. 416)

using the canonical definitions of groups (cf. p. 359) and of XOR (cf. p. 358). 
Furthermore, for the canonical definition of groups the proof is given that 
every group has a unique identity element (cf. p. 359 ff.), and this property 
is then transferred to the XOR group by performing basically only a few 
substitutions (cf. pp. 417 ff.).

The expression of the relationship between a canonical definition and a 
specific instance in dependent type theory has a number of advantages:
1. It does not require a meta-theory (an additional theory layer on top of the 
formal/object language) such as, for example, model theory, since the 
relationship can be expressed _within_ the formal language (object language) 
itself (in philosophy this would be called "immanent").
2. It does not use (axiomatic) set theory.
3. It does not require the Axiom of Choice (which exists neither in Q0 nor in 
R0).
For the critique of the concept of meta-theory and of model theory, cf. 
[Kubota, 2013, pp. 13 ff.].
For the critique of the concept of meta-theory and of (axiomatic) set theory, 
see also
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-December/msg00042.html

Please note that seeking an "explicit description of certain tasks typically 
executed at an implicit, intuitive level by mathematicians" [Mochizuki, 2015, 
p. 66] is the aim of type theory - there are nearly identical formulations in 
the work of Andrews - and that "the emphasis in the theory of species lies in 
the programs — i.e., 'software' — that yield the desired output data, not on 
the output data itself" [Mochizuki, 2015, p. 69] is also one of the key 
features of lambda-calculus. For comparison, the corresponding quote in 
Andrews' work is: "[M]ost mathematicians do make mental distinctions between 
different types of mathematical objects, and use different types of letters to 
denote them, so it might be claimed that type theory provides a more natural 
formalization of mathematics as it is actually practiced. In addition, explicit 
syntactic distinctions between expressions denoting intuitively different types 
of mathematical entities are very useful in computerized systems for exploring 
and applying mathematics [...]." [Andrews, 2002, p. 205]

3. Expressiveness vs. automation

The main notion of proof verification, as done by the R0 implementation, is 
"expressiveness", focusing on principle (philosophical) questions such as 
expressibility, definability or provability without regard to practical 
criteria such as efficiency or automation in carrying out proofs. Hence proof 
verification is very close to establishing a logistic system like Q0 or R0, 
"finding a formulation of type theory which is as expressive as possible, 
allowing mathematical ideas to be expressed precisely with a minimum of 
circumlocutions, and which is as simple and economical as is possible without 
sacrificing expressiveness." [Andrews, 2002, p. 205]

Ramana Kumar's statement that "there are already several variations of theorem 
provers implementing a roughly equivalent logic", e.g., "Isabelle/HOL, HOL4, 
HOL Light", is correct if one considers logical equivalence only. But the aim 
here is to find the most adequate or natural formulation. In most cases this 
coincides with "The Principle of Reductionism" [Kubota, 2015, p. 11]. For 
example, "HOL Light [...] has 'ten primitive rules of inference' [Harrison, 
2009, p. 61]" [Kubota, 2015, p. 14], but Q0 has only a single one.

For this reason, I emphasized the definability of any well-formed formula 
(including all connectives and quantifiers) and derivability of any rule 
(including the rule of modus ponens) on the basis of only a very small set of 
primitive symbols and rules, namely
- a single rule of inference,
- a single variable binder,
- only two primitive constants, and
- only two primitive types
in the presentation of Q0 at
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00147.html

Furthermore, since natural deduction requires more rules of inference than 
axiomatic (Hilbert-style) deductive systems, Hilbert-style logistic systems 
like Q0 are the preferred choice for finding a formulation of type theory as 
discussed above.

Like Church's type theory [cf. Church, 1940] known for its "precise formulation 
of the syntax" [Paulson, 1989, p. 5], Andrews' Q0 is known for its precision 
and accuracy due to its simple, clean and elegant design. "Church formalizes 
syntax, including quantifiers, in the typed [lambda]-calculus. His technique is 
now standard in generic theorem proving. See [...] Andrews [1] for the formal 
development." [Paulson, 1989, p. 5]

Andrews' definition of "the universal quantifier [...] defined in terms of 
truth" [Paulson, 1989, p. 14] has gained Paulson's attention, and in dependent 
type theory one can also add type abstraction. For comparison, see:
	http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-175.pdf (p. 14)
	http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf (p. 356)

Another example for the precision of the formal language is the 
non-definability (non-expressibility) of a Goedel numbering (or encoding) 
function within Q0 or R0. Isabelle/HOL currently lacks this precision as shown 
at
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-January/msg00029.html

4. Natural deduction and logical framework (Isabelle et al.)

However, for the practical purpose of automation, natural deduction provides 
the huge advantage of making metatheorems symbolically representable instead 
of, for example, only applying proof templates via recursive file inclusion as 
in the R0 implementation. So if Paulson writes: "Natural deduction is far 
superior for automated proof." [Paulson, 1989, p. 3], this is obviously true, 
but only half of the truth; the other half of the truth is that the precision 
of Hilbert-style systems (i.e., Church and Andrews) is lost when opting for 
natural deduction. Hence the decision between Hilbert-style systems and natural 
deduction is a question of weighting the advantages and disadvantages depending 
on the purpose (proof verification vs. automated deduction), and furthermore, 
in the case of natural deduction, additional measures have to be taken in order 
to preserve the strict distinctions between the logical levels. So for proof 
verification I would advise axiomatic (Hilbert-style) deductive systems, and 
for automated deduction natural deduction, but in the latter case the 
additional measures are important.

A logical framework provides the means to implement several object logics, 
which is not necessary if one regards R0 as the natural and ideal logic. 
Practical reasons, such as re-using existing source code, may be relevant, 
however, in general "I would advise against using some kind of meta-logic or 
meta-language, as additional features may weaken the rigor of (or even create 
an inconsistency in) the logical kernel" as stated earlier at
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-December/msg00018.html
But there is no principle objection if additional measures are taken in order 
to preserve the strict distinctions between the logical levels as specified at
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-January/msg00029.html

Additional measures have to be implemented in both a concrete and a general way.

a) At the concrete level, for the choice of
- natural deduction (with the danger of not distinguishing levels 2 and 3) such 
an implementation seems to be, at the first glance, provided with schematic 
(syntactical) variables, and with "Meta-logic" [Nipkow, 2015, p. 11] operators 
having a lower precedence than the "Logic" [Nipkow, 2015, p. 11] operators, but 
for the choice of
- a logical framework (with the danger of not distinguishing levels 1 and 2) 
not, since the metamathematical notion "term" (level 1) is treated as a 
concrete mathematical type symbol (level 2) in Paulson's presentation of 
Goedel's First Incompleteness Theorem.

b) At the general level, the implementation of automated deduction can receive 
its philosophical legitimation only through the ideal formulation of type 
theory as expressed by Andrews quoted above. This can be achieved by 
establishing a one-to-one correspondence between the theorems/metatheorems of 
the implementations of both automated deduction and proof verification, ideally 
by a metamathematical proof arithmetizing both systems, or at least by 
comparison of canonical definitions and proofs. My preference would be the 
generation of R0 code by proofs obtained in Isabelle/HOL, such that the 
Isabelle/HOL proofs could be verified by the R0 implementation.

If there are any further e-mail comments, please allow me to postpone answers 
where appropriate until my forthcoming publication of R0 [cf. Kubota, 2015].

Kind regards,

Ken Kubota

References

Andrews, Peter B. (2002), An Introduction to Mathematical Logic and Type 
Theory: To Truth Through Proof. Second edition. Dordrecht / Boston / London: 
Kluwer Academic Publishers. ISBN 1-4020-0763-9. DOI: 10.1007/978-94-015-9934-4.

Church, Alonzo (1940), "A Formulation of the Simple Theory of Types". In: 
Journal of Symbolic Logic 5, pp. 56-68.

Gödel, Kurt (1931), "On formally undecidable propositions of Principia 
mathematica and related systems I". In: Heijenoort, Jean van, ed. (1967), From 
Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931. Cambridge, 
Massachusetts: Harvard University Press, pp. 596-616.

Kubota, Ken (2013), On Some Doubts Concerning the Formal Correctness of Gödel's 
Incompleteness Theorem. Berlin: Owl of Minerva Press. ISBN 978-3-943334-04-3. 
DOI: 10.4444/100.101. See: http://dx.doi.org/10.4444/100.101

Kubota, Ken (2015), On the Theory of Mathematical Forms (Draft of May 18, 
2015). Unpublished manuscript. SHA-512: a0dfe205eb1a2cb29efaa579d68fa2e5 
45af74d8cd6c270cf4c95ed1ba6f7944 fdcffaef2e761c8215945a9dcd535a50 
011d8303fd59f2c8a4e6f64125867dc4. DOI: 10.4444/100.10. See: 
http://dx.doi.org/10.4444/100.10

Kubota, Ken (2015a), Excerpt from [Kubota, 2015] (pp. 356-364, pp. 411-420, and 
pp. 754-755). Available online at 
http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf 
(January 24, 2016). SHA-512: 67a48ee12a61583bd82c286136459c0c 
9fd77f5fd7bd820e8b6fe6384d977eda 4d92705dac5b3f97e7981d7b709fc783 
3d1047d1831bc357eb57b263b44c885b.

Mochizuki, Shinichi (2015), "Inter-universal Teichmuller Theory IV: Log-volume 
Computations and Set-theoretic Foundations" (December 2015). Available online 
at 
http://www.kurims.kyoto-u.ac.jp/~motizuki/Inter-universal%20Teichmuller%20Theory%20IV.pdf 
(January 24, 2016). SHA-512: 93372b4acba90195fc6ffc2e16830464 
b3bf27c4bdea156a915d3e7e5fdaad2a 4c85d0e1917064a8afd59e1a3af29a70 
a438252bf2cfcdb90b12cd20f272c179.

Nipkow, Tobias (2015), "What's in Main" (May 25, 2015). Available online at 
https://isabelle.in.tum.de/dist/Isabelle2015/doc/main.pdf (January 24, 2016).

Paulson, Lawrence C. (1989), "A Formulation of the Simple Theory of Types (for 
Isabelle)". Available online at 
http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-175.pdf (January 24, 2016).

____________________

Ken Kubota
doi: 10.4444/100
http://dx.doi.org/10.4444/100

------------------------------------------------------------------------------
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=267308311&iu=/4140
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Martin Leucker | 23 Jan 12:48 2016
Picon

CfP: ICTAC 2016


**********************************************************************
CALL FOR PAPERS -- ICTAC 2016
13th International Colloquium on Theoretical Aspects of Computing
24-31 October 2016, Taipei, Taiwan, ROC
http://cc.ee.ntu.edu.tw/~ictac2016

DEADLINE FOR ABSTRACT SUBMISSIONS: 23 APRIL, 2016
**********************************************************************

ICTAC 2016 will be held in the Department of Electrical Engineering,
National Taiwan University, Taipei, Taiwan, ROC, during the period 24-31
October, 2016.

Established in 2004, the ICTAC conference series aims at bringing
together practitioners and researchers from academia, industry and
government to present research and to exchange ideas and experience
addressing challenges in both theoretical aspects of computing and in
the exploitation of theory through methods and tools for system
development. ICTAC also aims to promote cooperation in research and
education between participants and their institutions, from developing
and industrial countries.

THEMES AND TOPICS OF PAPERS

Topics of interest include theories of computation and programming,
foundations of software engineering and formal techniques in software
design and verification, as well as tools that support formal techniques
for system modeling, design and verification.

The topical areas of the conference include, but are not limited to
* Automata theory and formal languages;
* Principles and semantics of programming languages;
* Theories of concurrency, mobility and reconfiguration;
* Logics and their applications;
* Software architectures and their models, refinement and verification;
* Relationship between software requirements, models and code;
* Program static and dynamic analysis and verification;
* Software specification, refinement, verification and testing;
* Model checking and theorem proving;
* Models of object and component systems;
* Coordination and feature interaction;
* Integration of theories, formal methods and tools for engineering
computing systems;
* Service-oriented architectures: models and development methods;
* Models of concurrency, security, and mobility;
* Theory of distributed, grid and cloud computing;
* Real-time, embedded, hybrid and cyber-physical systems;
* Type and category theory in computer science;
* Models for learning and education;
* Case studies, theories, tools and experiments of verified systems;
* Domain-specific modeling and technology: examples, frameworks and
experience.
* Challenges and foundations in the environmental modeling and
monitoring, healthcare, and disaster management.

INVITED SPEAKERS

* Hsu-Chun Yen, National Taiwan University (TW)
* Leonardo de Moura, Microsoft (US)
* Heike Wehrheim, Universität Paderborn (DE)

ASSOCIATED EVENT

* ICTAC Summer School on Formal Methods (29-31 October, 2016)

IMPORTANT DATES

* Abstract submission: 23 April, 2016
* Paper submission: 1 May, 2016
* Author notification: 20 June, 2016
* Camera ready: Monday, 15 July, 2015

PAPER CATEGORIES AND FORMAT

We call for submissions, related to the above areas and topics,
according to the following three categories:
* Regular papers, with original research contributions;
* Short papers, on recent work or proposals of emerging challenges;
* Tool papers, on tools that support formal techniques for software
modeling, system design and verification. Submissions should adhere to
the LNCS format (see http://www.springer.de/comp/lncs/authors.html for
details). Regular papers should not exceed 18 pages. Short and tool
papers should not exceed 10 pages.

Submissions to the colloquium must not have been published or be
concurrently considered for publication elsewhere. All submissions will
be judged on the basis of originality, contribution to the field,
technical and presentation quality, as well as their relevance to the
conference.

SUBMISSION LINK

www.easychair.org/conferences/?conf=ictac2016

PROCEEDINGS

As for the past editions, the plan is to publish the proceedings of
ICTAC 2016 with Springer in the series Lecture Notes in Computer Science
(LNCS).

SPECIAL ISSUE

Extended versions of selected papers from ICTAC 2015 will be invited to
a special issue in a journal that will be announced later.

GENERAL CHAIR

* Farn Wang, National Taiwan University (TW)

PROGRAMME COMMITTEE CHAIRS

* Augusto Sampaio, Universidade Federal de Pernambuco, Brazil
* Farn Wang, National Taiwan University, Taiwan

PROGRAMME COMMITTEE

* Bernhard Aichernig, TU Graz, Austria
* Farhad Arbab, CWI and Leiden University, Netherlands
* Mauricio Ayala-Rincón, Universidade de Brasilia, Brazil
* Mário Benevides, Universidade Federal do Rio de Janeiro, Brazil
* Ana Cavalcanti, University of York, UK
* Yu-Fang Chen, Academia Sinica, Taiwan
* Gabriel Ciobanu, Institute of Computer Science, Romania
* Hung Dang-Van, Vietnam National University, Vietnam
* Rocco DeNicola, Institute for Advanced Studies Lucca, Italy
* Razvan Diaconescu, IMAR, Romania
* Jin-Song Dong, National University of Singapore, Singapore
* José Fiadeiro, University of London, UK
* John Fitzgerald, Newcastle University, UK
* Marcelo Frias, Buenos Aires Institute of Technology, Argentina
* Martin Fränzle, Universität Oldenburg, Germany
* Lindsay Groves, Victoria University of Wellington, New Zeland
* Zhenjiang Hu, NII, Japan
* Jie-Hong Jiang, National Taiwan University, Taiwan
* Cliff Jones, Newcastle University, UK
* Luis Lamb, Universidade Federal do Rio Grande do Sul, Brazil
* Kim Larsen, Aalborg University, Denmark
* Martin Leucker, University of Lübeck, Germany
* Zhiming Liu, Southwest University in Chongqing, China
* Ana Melo, Universidade de São Paulo, Brazil
* Dominique Méry, Université de Lorraine, France
* Alexandre Mota, Universidade Federal de Pernambuco, Brazil
* Mohammad Mousavi, Halmstad University, Sweden
* Tobias Nipkow, TU München, Germany
* José Oliveira, Universidade do Minho, Portugal
* Catuscia Palamidessi, INRIA, France
* Paritosh Pandya, Tata Institute of Fundamental Research, India
* António Ravara, Universidade Nova de Lisboa, Portugal
* Camilo Rueda, Universidad Javeriana, Colombia
* Jacques Sakarovitch, CNRS / Telecom ParisTech, France
* Augusto Sampaio (PC co-chair), Universidade Federal de Pernambuco, Brazil
* Martin Schaef, SRI International, US
* Sven Schewe, University of Liverpool, UK
* Emil Sekerinski, McMaster University, Canada
* Hiroyuki Seki, Nagoya University, Japan
* Tetsuo Shibuya, University of Tokyo, Japan
* Andrzej Tarlecki, Warsaw University, Poland
* Kazunori Ueda, Waseda University, Japan
* Frank Valencia, Ecole Polytechnique, France
* Farn Wang (PC co-chair), National Taiwan University, Taiwan
* Jim Woodcock, University of York, UK
* Hsu-Chun Yen, National Taiwan University, Taiwan
* Shoji Yuen, Nagoya University, Japan
* Naijun Zhan, Chinese Academy of Sciences, China
* Lijun Zhang, Chinese Academy of Sciences, China
* Huibiao Zhu, East China Normal University, China

STERRING COMMITTEE

* Ana Cavalcanti, University of York, UK
* Martin Leucker, University of Luebeck, Germany
* Zhiming Liu,  Southwest University  in Chongqing, China
* Tobias Nipkow, Technical University Munich, Germany
* Augusto Sampaio, Federal University of Pernambuco, Brazil
* Natarajan Shankar, SRI International, US
------------------------------------------------------------------------------
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=267308311&iu=/4140
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Havelund, Klaus (349F | 18 Jan 20:19 2016
Picon
Picon

[fm-announcements] RV 2016, Sept 23-30 2016, Madrid, Spain - 1st Call for Papers and Tutorials

RV 2016

16th International Conference on Runtime Verification

September 23-30, Madrid, Spain


Scope

Runtime verification is concerned with monitoring and analysis of software and hardware system executions. Runtime verification techniques are crucial for system correctness, reliability, and robustness; they are significantly more powerful and versatile than conventional testing, and more practical than exhaustive formal verification. Runtime verification can be used prior to deployment, for testing, verification, and debugging purposes, and after deployment for ensuring reliability, safety, and security and for providing fault containment and recovery as well as online system repair. Topics of interest to the conference include:

- specification languages
- specification mining
- program instrumentation
- monitor construction techniques
- logging, recording, and replay
- runtime enforcement, fault detection, localization, containment, recovery and repair
- program steering and adaptation
- metrics and statistical information gathering
- combination of static and dynamic analyses
- program execution visualization
- monitoring techniques for safety/mission-critical systems
- monitoring distributed systems, cloud services, and big data applications
- monitoring security and privacy policies

Application areas of runtime verification include cyber-physical systems, safety/mission-critical systems, enterprise and systems software, autonomous and reactive control systems, health management and diagnosis systems, and system security and privacy.

Invited Speakers

The program of RV 2016 will feature invited talks from:

  • Gul Agha (University of Illinois at Urbana-Champaign, USA)
  • Oded Maler (CNRS and University of Grenoble-Alpes, France)
  • Fred B. Schneider (Cornell University, USA)

Overview

RV 2016 will be held September 23-30 in Madrid, Spain. RV 2016 will feature the first summer school on Runtime Verification (September 23-25), two workshop days (September 26-25), and three conference days (September 28-30).

General Information on Submissions

All papers and tutorials will appear in the conference proceedings in an LNCS volume. Submitted papers and tutorials must use the LNCS/Springer style. At least one author of each accepted paper and tutorial must attend RV 2016 to present the paper. Papers must be written in English and submitted electronically (in PDF format) using the EasyChair system. The below page limitations include all text and figures, but exclude references. Additional details omitted due to space limitations may be included in a clearly marked appendix that will be reviewed at the discretion of reviewers.

Research Papers Track

Research papers can be submitted in two categories: regular and short papers. Papers in both categories will be reviewed by at least 3 members of the Program Committee.
  • Regular Papers (up to 15 pages) should present original unpublished results. Theoretical papers, system and application papers as well as case studies on runtime verification are all welcome.
    The Program Committee of RV 2015 will give a best paper award. A selection of accepted regular papers will be invited to appear in a special issue of the Springer Journal on Formal Methods in System Design.
  • Short Papers (up to 6 pages) may present novel but not necessarily thoroughly worked out ideas, for example emerging runtime verification techniques and applications, or techniques and applications that establish relationships between runtime verification and other domains. Accepted short papers will be presented in special talk (15 minutes) and poster sessions.

Tool Papers Track

The aim of the RV 2016 tool track is to provide an opportunity for researchers and practitioners to show and to discuss the latest advances, experiences and challenges in devising and developing reliable software tools for runtime verification. All tool papers will be reviewed by at least 3 members of the Tool Committee. An author of each accepted tool paper should give a 15-20 minutes demonstration during the conference.

All tool papers must include information on tool availability, maturity, selected experimental results and it should provide a link to a website containing the theoretical background and user guide. Furthermore, we strongly encourage authors to make their tools and benchmarks available with their submission.
We encourage tool papers to include a script in an appendix (not included in the page count) describing how the demo will be conducted during the conference presentation with screenshots presenting step-by-step the tool’s capabilities, highlighting the main characteristics and the usage.

Tool papers can be submitted into two categories:

  • Regular Tool Papers (up to 8 pages). A tool paper in this category should present a new tool, a new tool component or significant and novel extensions to existing tools supporting runtime verification. Each submission should be original and not published previously in a tool paper form.
  • Tool Exhibition Papers (up to 4 pages). A tool paper in this category can have been previously published. A tool paper in this category should be oriented towards the tool usage and is an opportunity for the developers to present them at RV 2016.

Tutorial Track

Tutorials are two-to-three-hour presentations on a selected topic. Additionally, tutorial presenters will be offered to publish a paper of up to 20 pages in the LNCS conference proceedings.

A proposal for a tutorial must contain the subject of the tutorial, a proposed timeline, a note on previous similar tutorials (if applicable) and the differences to this incarnation, and a biography of the presenter. The proposal must not exceed 2 pages. Tutorial proposals will be reviewed by the Program Committee.

Important Dates

Research and tool papers as well as tutorials will follow the following timeline:

  • Abstract deadline: May 8, 2016
  • Paper and tutorial deadline: May 15, 2016
  • Tutorial notification: June 1, 2016
  • Paper notification: July 11, 2016
  • Camera ready deadline: August 8, 2016
  • Summer school: September 23-25, 2016
  • Workshops and tutorials: September 26-27, 2016
  • Conference: September 28-30, 2016

Committees

Program Committee Chairs


  • Yliès Falcone, Univ. Grenoble-Alpes and Inria, France
  • Cesar Sanchez, IMDEA Software, Madrid, Spain

Tool Committee Chair


  • Klaus Havelund, NASA Jet Propulsion Laboratory, USA

Local Organization Chair


  • Juan E. Tapiador, Universidad Carlos III de Madrid, Spain

Program Committee


  • Erika Abraham, RWTH Aachen University, Germany
  • Howard Barringer, The University of Manchester, UK
  • Ezio Bartocci, TU Wien, Austria
  • Andreas Bauer, NICTA & Australian National University, Australia
  • Saddek Bensalem, Univ. Grenoble Alpes, France
  • Eric Bodden, Fraunhofer SIT and Technische University Darmstadt, Germany
  • Borzoo Bonakdarpour, McMaster University, Canada
  • Laura Bozzelli, Technical University of Madrid (UPM), Spain
  • Juan Caballero, IMDEA Software Institute, Spain
  • Wei-Ngan Chin, National University of Singapore, Singapore
  • Christian Colombo, University of Malta, Malta
  • Jyotirmoy Deshmukh, Toyota Technical Center, USA
  • Alexandre Donzé, UC Berkeley EECS Department, USA
  • Yliès Falcone, Univ. Grenoble Alpes and Inria, France
  • Bernd Finkbeiner, Saarland University, Germany
  • Adrian Francalanza, University of Malta, Malta
  • Vijay Garg, The University of Texas at Austin, USA
  • Patrice Godefroid, Microsoft Research, USA
  • Susanne Graf, Univ. Grenoble Alpes and CNRS, France
  • Radu Grosu, Vienna University of Technology, Austria
  • Sylvain Hallé, Université du Québec à Chicoutimi, Canada
  • Klaus Havelund, NASA Jet Propulsion Laboratory, USA
  • Johan Jaffar, National University of Singapore, Singapore
  • Thierry Jéron, Inria Rennes – Bretagne Atlantique, France
  • Johannes Kinder, Royal Holloway University of London, UK
  • Felix Klaedtke, NEC Europe Ltd., Germany
  • Kim G. Larsen, Aalborg University, Denmark
  • Axel Legay, Inria Rennes – Bretagne Atlantique, France
  • Martin Leucker, University of Lübeck, Germany
  • Benjamin Livshits, Microsoft Research, USA
  • Joao Lourenço, Universidade Nova de Lisboa, Portugal
  • Rupak Majumdar, MPI-SWS, Germany
  • Leonardo Mariani, University of Milano Bicocca, Italy
  • David Naumann, Stevens Institute of Technology, USA
  • Dejan Nickovic, Austrian Institute of Technology, Austria
  • Gordon Pace, University of Malta, Malta
  • Doron Peled, Bar Ilan University, Israel
  • Lee Pike, Galois, Inc., USA
  • Grigore Rosu, University of Illinois at Urbana-Champaign, USA
  • Gwen Salaün, Univ. Grenoble Alpes and Inria, France
  • Cesar Sanchez, IMDEA Software Institute, Spain
  • Sriram Sankaranarayanan, University of Colorado Boulder, USA
  • Gerardo Schneider, University of Gothenburg, Sweden
  • Scott Smolka, Stony Brook University, USA
  • Oleg Sokolsky, University of Pennsylvania, USA
  • Bernhard Steffen, University of Dortmund, Germany
  • Scott Stoller, Stony Brook University, USA
  • Volder Stolz, University of Oslo, Norway
  • Jun Sun, Singapore University of Technology and Design, Singapore
  • Juan Tapiador, Universidad Carlos III de Madrid, Spain
  • Serdar Tasiran, Koc Univ., Turkey
  • Michael Whalen, University of Minnesota, USA
  • Eugen Zalinescu, ETH Zurich, Switzerland
  • Lenore Zuck, University of Illinois at Chicago, USA

Tool Committee


  • Steven Artz, EC Spride, Germany
  • Howard Barringer, The University of Manchester, UK
  • Ezio Bartocci, TU Wien, Austria
  • Martin Leucker, University of Luebeck, Germany
  • Gordon Pace, University of Malta, Malta
  • Giles Reger, The University of Manchester, UK
  • Julien Signoles, CEA, France
  • Oleg Sokolsky, University of Pennsylvania, USA
  • Bernhard Steffen, University of Dortmund, Germany
  • Nikolai Tillmann, Microsoft Research, USA
  • Eugen Zalinescu, ETH Zurich, Switzerland
Attachment (cfp.pdf): application/pdf, 312 KiB
---
To opt-out from this mailing list, send an email to

fm-announcements-request <at> lists.nasa.gov

with the word 'unsubscribe' as subject or in the body. You can also make the request by contacting

fm-announcements-owner <at> lists.nasa.gov 
------------------------------------------------------------------------------
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=267308311&iu=/4140
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Geoff Sutcliffe | 15 Jan 18:29 2016
Picon

UNIF 2016 - Call for Papers

UNIF 2016  - Call for papers

The 30th International Workshop on Unification is the 30th event in a series 
of international meetings devoted to unification theory and its applications.
Unification is concerned with the problem of making two terms equal, finding 
solutions for equations, or making formulas equivalent. It is a fundamental 
process used in a number of fields of computer science, including automated 
reasoning, term rewriting, logic programming, natural language processing, 
program analysis, types, etc. 

The International Workshop on Unification (UNIF) is a yearly forum for 
researchers in unification theory and related fields to meet old and new 
colleagues, to present recent (even unfinished) work, and to discuss new 
ideas and trends. It is also a good opportunity for young researchers and 
scientists working in related areas to get an overview of the current state 
of the art in unification theory. The workshop will be  hosted by the 1st 
International Conference on Formal Structures for Computation and Deduction 
(FSCD, Porto, June 2016)

Description of the Topic
------------------------
Unification is one of the central notions in automated reasoning and lies at 
the heart of many reasoning systems. Unification is concerned with the problem 
of making two terms equal, either syntactically or modulo a theory. UNIF 2016 
will be the 30th in a series of annual international workshops on unification. 
Previous editions have taken place mostly in Europe (Austria, Denmark, France, 
Germany, Ireland, Italy, Poland, UK), but also in the USA and Japan. For more 
details on previous UNIF workshops, please see the UNIF homepage at
    http://www.pps.jussieu.fr/~treinen/unif/.
Traditionally, the scope of the UNIF workshops has covered the topic of
unification in a broad sense, encompassing also research in constraint solving,
admissibility of inference rules, and applications such as type checking, 
query answering and cryptographic protocol analysis. A non-exhaustive list 
of topics of interest includes:
+ Unification algorithms, calculi and implementations
+ Equational unification and unification modulo theories
+ Unification in modal, temporal and description logics
+ Admissibility of Inference Rules
+ Narrowing
+ Matching algorithms
+ Constraint solving
+ Combination problems
+ Disunification
+ Higher-Order Unification
+ Type checking and reconstruction
+ Typed unification
+ Complexity issues
+ Query answering
+ Implementation techniques
+ Applications of unification
+ Antiunification/Generalization

Submission Details
------------------
Following the tradition of UNIF, we call for submissions of abstracts (5 pages)
in EasyChair style, to be submitted electronically as PDF files through the 
EasyChair submission site:
    https://easychair.org/conferences/?conf=unif2016

Abstracts will be evaluated by the Programme Committee (if necessary with 
support from external reviewers) regarding their significance for the 
workshop. Accepted abstracts will be presented at the workshop and included 
in the informal proceedings of the workshop, available in printed form at 
the workshop and in electronic form from the UNIF homepage:
    http://www.pps.jussieu.fr/~treinen/unif/

Based on the number and quality of submissions we will decide whether to
organize a special journal issue.

Important Dates
---------------
+ Paper Submission: May 1, 2016
+ Notif. of Acceptance: May 29 2016
+ Final version: June 5, 2016
+ Conference: June 26, 2016

Organizers
----------
Silvio Ghilardi
Department of Mathematics
Universite degli Studi di Milano
Milano, Italy
email: silvio.ghilardi <at> unimi.it
homepage: http://users.mat.unimi.it/users/ghilardi/
phone: +39 02 5031 6142

Manfred Schmidt-Schauss
Department of Computer Science and Mathematics
Goethe University
Frankfurt, Germany
email: schauss <at> ki.informatik.uni-frankfurt.de
homepage: http://www.ki.informatik.uni-frankfurt.de
phone: +49 69 798 2859

------------------------------------------------------------------------------
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=267308311&iu=/4140
Carlo A. Furia | 18 Jan 19:56 2016
Picon
Picon

TAP 2016 (Tests & Proofs): Final CfP

================================================
  TAP 2016
  10th International Conference on Tests & Proofs

   5-7 July 2016, Vienna, Austria
   Co-located with STAF 2016

   http://tap2016.ist.tugraz.at

   Final Call for Papers
================================================

NEW: submission deadline approaching!
NEW: industrial invited speaker: Klaus Reichl, Thales

   * Abstracts: 29 January 2016
   * Papers: 5 February 2016
   * Notifications: 15 April 2016
   * Camera ready versions: 6 May 2016

The TAP conference promotes research in verification and formal
methods that targets the interplay of proofs and testing: the
advancement of techniques of each kind and their combination, with the
ultimate goal of improving software and system dependability.

Dijkstra's famous remark that "testing shows the presence, not the
absence of bugs" contributed to reinforcing the opinion that program
testing and program proving are antithetical techniques. Under the
traditional view, proving aims at establishing correctness, whereas
testing aims at uncovering errors: a correct program needs no testing,
and there's no point in trying to prove a buggy one. As a result,
research in verification has historically been divided into separate
communities, with only few interested in both testing and proving.

This attitude has changed significantly over the last
decade. Verification research has seen a convergence of heterogeneous
techniques and a synergy between traditionally distinct
communities. Testing and proving are increasingly seen as
complementary rather than mutually exclusive techniques: formal
testing can increase the confidence in the correctness of program
parts that are hard to reason about formally, and proving can help
make testing more efficient and systematic.

The TAP conference aims to promote research in the intersection of
testing and proving by bringing together researchers and practitioners
from both areas of verification.

Scope & Topics
--------------

TAP's scope encompasses many aspects of verification technology,
including foundational work, tool development, and empirical
research. Its topics of interest center around the connection between
proofs (and other static techniques) and testing (and other dynamic
techniques). Papers are solicited on, but not limited to, the
following topics:

   * Verification and analysis techniques combining proofs and tests

   * Program proving with the aid of testing techniques

   * Deductive techniques (theorem proving, model checking, symbolic
     execution, SMT solving, constraint logic programming, etc.) to
     support testing: generating testing inputs and oracles, supporting
     coverage criteria, and so on.

   * Program analysis techniques combining static and dynamic analysis

   * Specification inference by deductive and dynamic methods

   * Testing and runtime analysis of formal specifications

   * Model-based testing and verification

   * Using model checking to generate test cases

   * Testing of verification tools and environments

   * Applications of testing and proving to new domains, such as
     security, configuration management, and language-based techniques

   * Bridging the gap between concrete and symbolic reasoning
     techniques

   * Innovative approaches to verification such as crowdsourcing and
     serious games

   * Case studies, tool and framework descriptions, and experience
     reports about combining tests and proofs

Submissions
-----------

TAP 2015 accepts regular-length research papers (16 LNCS pages +
references), short papers (6 LNCS pages + references), and tool
demonstration papers (8 LNCS pages + references). For details, see the
submission instructions: http://tap2016.ist.tugraz.at/submission.shtml

Authors of selected papers will be invited to submit extended versions
of their TAP 2016 papers for a special issue of the Springer journal
Formal Aspects of Computing (http://link.springer.com/journal/165).

Industrial invited speaker
--------------------------

Klaus Reichl, Thales, Vienna, Austria

Organization
------------

PC Chairs:

   * Bernhard K. Aichernig, Graz University of Technology, Austria
   * Carlo A. Furia, Chalmers University of Technology, Sweden

Program Committee:

   * Jasmin C. Blanchette, Inria Nancy and MPI Saarbruecken, France and
     Germany
   * Achim D. Brucker, SAP AG, Germany
   * Catherine Dubois, ENSIIE, France
   * Gordon Fraser, University of Sheffield, UK
   * Juan Pablo Galeotti, University of Buenos Aires, Argentina
   * Angelo Gargantini, Universita di Bergamo, Italy
   * Alain Giorgetti, FEMTO-ST Institute and University of
      Franche-Comte, France
   * Christoph Gladisch, Bosch GmbH, Germany
   * Martin Gogolla, University of Bremen, Germany
   * Arnaud Gotlieb, Simula Research Laboratory, Norway
   * Ashutosh Gupta, Tata Institute, Mumbai, India
   * Reiner Haehnle, TU Darmstadt, Germany
   * Marieke Huisman, University of Twente, the Netherlands
   * Bart Jacobs, KU Leuven, Belgium
   * Nikolai Kosmatov, CEA LIST, France
   * Laura Kovacs, Chalmers and TU Wien, Sweden and Austria
   * Shaoying Liu, Hosei University, Japan
   * Panagiotis (Pete) Manolios, Northeastern University, USA
   * Karl Meinke, KTH, Sweden
   * Brian Nielsen, Aalborg University, Denmark
   * Nadia Polikarpova, MIT, USA
   * Andrew J. Reynolds, EPFL, Switzerland
   * Augusto Sampaio, Federal University of Pernambuco, Brazil
   * Martina Seidl, Johannes Kepler University Linz, Austria
   * Jun Sun, Singapore University of Technology and Design, Singapore
   * Nikolai Tillmann, Microsoft, USA
   * T. H. Tse, the University of Hong Kong, Hong Kong
   * Margus Veanes, Microsoft Research Redmond, USA
   * Burkhart Wolff, University of Paris-Sud, France

------------------------------------------------------------------------------
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=267308311&iu=/4140
Roopsha Samanta | 20 Jan 14:21 2016
Picon

CFP: CAV 2016, July 17-23, Toronto [Abstract Submission: Jan 24]

Apologies for multiple copies of this CFP.

***************************************************************
*                  28th International Conference
*                                     on
*            Computer Aided Verification (CAV 2016)
*
*                         July 17-23, 2016
*                   Toronto, Ontario, Canada
*
*                         Call for Papers
*
*                      http://i-cav.org/2016/
****************************************************************

Important Dates
----------------------
All deadlines are 4pm EST.

Abstract submission:         January 24, 2016 (coming Sunday)
Paper submission:             January 29, 2016 (Friday)
Author response period:    March 23-25, 2016 (Wednesday-Friday)
Author Notification:            April 15, 2016 (Friday)
Conference:                       July 17-23, 2016

Scope
--------

CAV 2016 is the 28th in a series dedicated to the advancement of the theory and
practice of computer-aided formal analysis methods for hardware and software
systems. CAV considers it vital to continue spurring advances in hardware and
software verification while expanding to new domains such as biological systems
and computer security. The conference covers the spectrum from theoretical
results to concrete applications, with an emphasis on practical verification
tools and the algorithms and techniques that are needed for their
implementation. The proceedings of the conference will be published in the
Springer LNCS series. A selection of papers will be invited to a special issue
of Formal Methods in System Design and the Journal of the ACM.

Topics of interest include but are not limited to:

* Algorithms and tools for verifying models and implementations
* Algorithms and tools for system synthesis
* Mathematical and logical foundations of verification and synthesis
* Specifications and correctness criteria for programs and systems
* Deductive verification using proof assistants
* Hardware verification techniques
* Program analysis and software verification
* Software synthesis
* Hybrid systems and embedded systems verification
* Compositional and abstraction-based techniques for verification
* Probabilistic and statistical approaches to verification
* Verification methods for parallel and concurrent systems
* Testing and run-time analysis based on verification technology
* Decision procedures and solvers for verification and synthesis
* Applications and case studies in verification and synthesis
* Verification in industrial practice
* New application areas for algorithmic verification and synthesis
* Formal models and methods for security
* Formal models and methods for biological systems

Paper Submission
------------------------

*** NEW this year: Double-blind submissions ***

Submissions on a wide range of topics are sought, particularly ones that
identify new research directions. CAV 2016 is not limited to topics discussed
in previous instances of the conference. Authors concerned about the
appropriateness of a topic may communicate by electronic mail with the
conference chairs prior to submission.

As explained below, CAV 2016 will follow a lightweight double-blind review
process. Submissions that are not "blinded" will be rejected without review.

Submissions will be in two categories: Regular Papers and Tool Papers.

* Regular Papers should not exceed 15 pages in LNCS format, not counting
references. These papers should contain original research and sufficient detail
to assess the merits and relevance of the contribution.  Papers will be
evaluated on basis of a combination of correctness, technical depth,
significance, novelty, clarity, and elegance. We welcome papers on theory, case
studies and comparisons with existing experimental research, as well as
combinations of new theory with experimental evaluation. A strong theoretical
paper is not required to have an experimental component. On the other hand,
strong papers reproducing and comparing existing results experimentally do not
require new theoretical insights.

* Tool Papers should not exceed 6 pages, not counting references. These papers
should describe system and implementation aspects of a tool with a large
(potential) user base (experiments not required, rehash of theory strongly
discouraged). Papers describing tools that have already been presented (in any
conference) will be accepted only if significant and clear enhancements to the
tool are reported and implemented.

Unlike last year, there is no separate Short Paper category.

Prior to the registration deadline, the authors will register their paper by
uploading information on the submission title, abstract (of at most 300 words),
authors, topics, and conflicts to the conference web site. Papers that are not
registered on time will be rejected.

We encourage authors to provide any supplementary material that is required to
support the claims made in the paper, such as detailed proofs or experimental
data. These materials should be uploaded at submission time, as a single pdf or
a tarball, not via a URL. It will be made available to reviewers only after
they have submitted their first-draft reviews and hence need not be anonymized.
Reviewers are under no obligation to look at the supplementary material but may
refer to it if they have questions about the material in the body of the paper.

Simultaneous submission to other conferences with proceedings or submission of
material that has already been published elsewhere is not allowed.

The review process will include a feedback/rebuttal period where authors will
have the option to respond to reviewer comments. The PC chairs may solicit
further reviews after the rebuttal period.

Papers must be submitted in PDF format. Submission will be via the HotCRP
system. The submission URL will be available on the website of the conference
closer to the deadline.

Lightweight Double-Blind Reviewing Process
-------------------------------------------------------------

CAV 2016 will employ a lightweight double-blind reviewing process. This means
that committee members will not have access to authors' names or affiliations
as they review a paper; however, authors' names will be revealed once reviews
have been submitted and online discussion has begun.

To facilitate this, submitted papers must adhere to two rules:

(1) author names and institutions must be omitted, and
(2) references to authors' own related work should be in the third person
(e.g., not "We build on our previous work ..." but rather "We build on the work
of ...").

The purpose of this process is to help the PC and external reviewers come to an
initial judgement about the paper without bias, not to make it impossible for
them to discover the authors if they were to try.  Nothing should be done in
the name of anonymity that weakens the submission or makes the job of reviewing
the paper more difficult (e.g., important background references should not be
omitted or anonymized). In addition, authors should feel free to disseminate
their ideas or draft versions of their paper as they normally would.  For
instance, authors may post drafts of their papers on the web or give talks on
their research ideas. A document answering frequently asked questions about the
double-blind review process is available on the conference website.


Artifact Evaluation
------------------------

Authors of accepted papers will be invited to submit their artifacts for
evaluation by a special committee.


Organizers
---------------

Chairs
---------
Swarat Chaudhuri, Rice University, USA
Azadeh Farzan, University of Toronto, Canada


CAV Award Committee
-------------------------------
Ahmed Bouajjani (Chair), Univ. Paris Diderot (Paris 7)
Tom Ball, Microsoft Research
Kim G. Larsen, Aalborg University
Natarajan Shankar, SRI International


Program Committee
---------------------------

Rajeev Alur, University of Pennsylvania
Christel Baier, Technische Universität Dresden
Clark Barrett, New York University
Roderick Bloem, Graz University of Technology
Pavol Cerny, University of Colorado, Boulder
Adam Chlipala, MIT
Alessandro Cimatti, Fondazione Bruno Kessler
Loris D'Antoni, University of Wisconsin, Madison
Constantin Enea, Univ. Paris Diderot (Paris 7)
Javier Esparza, Technische Universität München
Kousha Etessami, University of Edinburgh
Susanne Graf, VERIMAG
Orna Grumberg, Technion
Franjo Ivancic, Google
Somesh Jha, University of Wisconsin, Madison
Ranjit Jhala, University of California, San Diego
Joost-Pieter Katoen, RWTH Aachen University
Zachary Kincaid, University of Toronto
Laura Kovacs, Chalmers University of Technology
Viktor Kuncak, EPFL
Marta Kwiatkowska, Oxford University
Shuvendu Lahiri, Microsoft Research
Akash Lal, Microsoft Research
Pete Manolios, Northeastern University
Kenneth McMillan, Microsoft Research
David Monniaux, VERIMAG
Kedar Namjoshi, Bell Labs, Alcatel-Lucent
David Parker, University of Birmingham
Corina Pasareneau, Carnegie Mellon Silicon Valley/NASA Ames
Ruzica Piskac, Yale University
Andreas Podelski, University of Freiburg
Shaz Qadeer, Microsoft Research
Andrey Rybalchenko, Microsoft Research
Mooly Sagiv, Tel Aviv University
Sriram Sankaranarayanan, University of Colorado, Boulder
Sanjit Seshia, University of California, Berkeley
Natasha Sharygina, University of Lugano
Sharon Shoham, Academic College of Tel-Aviv Yaffo
Armando Solar-Lezama, MIT
Fabio Somenzi, University of Colorado, Boulder
Serdar Tesiran, Koç University
Mahesh Viswanathan, University of Illinois, Urbana-Champaign
Bow-Yaw Wang, Academia Sinica
Thomas Wies, New York University
Lenore Zuck, University of Illinois, Chicago


Workshop Chair
----------------------
Zachary Kincaid, University of Toronto, Canada


Artifact Evaluation Chair
--------------------------------
Aws Albarghouthi, University of Wisconsin, USA


Publicity Chair
-------------------
Roopsha Samanta, IST, Austria


Sponsorship Chair
-------------------
Pavol Cerny, University of Colorado, Boulder


Steering Committee
---------------------------
Michael Gordon, University of Cambridge, UK
Orna Grumberg, Technion, Israel
Aarti Gupta, Princeton University, USA
Kenneth McMillan, Microsoft Research, USA

------------------------------------------------------------------------------
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=267308311&iu=/4140
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Alwen Tiu | 20 Jan 03:36 2016
Picon

Postdoc position on hardware verification at NTU Singapore

[Apology for multiple postings]

One postdoc position is available at the School of Computer Engineering, Nanyang Technological University (NTU)  Singapore, for a project on hardware verification. 

Candidates must possess a PhD degree in Computer Science or related areas. The position is part of a larger project on formal verification of hardware and software systems at NTU. For this particular position, the postdoc is expected to work on building formal models of hardware description languages, and verifying the correctness of hardware designs. Candidates for the position must have experience in theorem proving tools. Candidates with knowledge of hardware design language are preferred. The salary range is between SGD 4000 - 6000 per month. 

The position will be initially offered for one year, but can be extended up to four years, subject to satisfactory performance and availability of funding. 

To apply for the position, please send a cover letter and your latest CV (please indicate names of three referees in your CV) by email to Alwen Tiu (atiu <at> ntu.edu.sgalwen.tiu <at> gmail.com). Applications will be accepted until the position is filled, but to ensure the full consideration of your application, please send your application by 21 February 2016. Only shortlisted candidates will be notified of the results of their applications. The selected candidate is expected to commence in April 2016.

If you have any further questions regarding the position and/or the project, please email atiu <at> ntu.edu.sg.


Regards,
Alwen Tiu
------------------------------------------------------------------------------
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=267308311&iu=/4140
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Alwen Tiu | 20 Jan 02:48 2016
Picon

Postdoc position on security protocol verification at NTU Singapore

One postdoc position is available at the School of Computer Engineering, Nanyang Technological University (NTU)  Singapore, for a project on verification of security protocols funded by the Ministry of Education of Singapore. 

A particular emphasis will be on designing and implementing decision procedures for finding attacks on protocols or producing formal proofs of their security. We will be using a mixture of process algebraic and logical frameworks to express protocols and their properties, in particular, equivalence properties of security protocols. 

Candidates must possess a PhD degree in Computer Science or related areas. Candidates with strong backgrounds in process calculus, such as the pi-calculus and its variants, and/or formal logic and theorem proving are preferred. The salary range is between SGD 4000 - 6000 per month. 

The position will be initially offered for one year, but can be extended up to three years, subject to satisfactory performance and availability of funding. 

To apply for the position, please send a cover letter and your latest CV (please indicate names of three referees in your CV) by email to Alwen Tiu (atiu <at> ntu.edu.sgalwen.tiu <at> gmail.com). Applications will be accepted until the position is filled, but to ensure the full consideration of your application, please send your application by 21 August 2015. Only shortlisted candidates will be notified of the results of their applications. The selected candidate is expected to commence in October 2015.

If you have any further questions regarding the position and/or the project, please email atiu <at> ntu.edu.sg.


Regards,
Alwen Tiu
------------------------------------------------------------------------------
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=267308311&iu=/4140
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Gmane