Re: [Hol-info] a question about rewrite in HOL4

[Michael Norrish]

> On 5 Mar 2016, at 09:01, Ramana Kumar  wrote:
>
> I think RW_TAC doesn't handle conditional rewrites very well. Try using rw or 
> simp instead.
>

RW_TAC handles conditional rewrites in exactly the same way as simp and rw.

If I try RW_TAC list_ss [cx_length] with the repository version of HOL, it 
solves the goal.

I turned the simplifier trace on to see the following steps taken:

[953932]:   rewriting LENGTH (cx l p q) with |- LENGTH p = LENGTH q ⇒ LENGTH 
(cx l p q) = LENGTH p
[970795]:   rewriting LENGTH p with  [.] |- LENGTH p = LENGTH q
[986129]:   rewriting LENGTH q = LENGTH q with |- x = x ⇔ T
[2857]:   rewriting LENGTH p with  [.] |- LENGTH p = LENGTH q
[20122]:   LENGTH q ≤ n via cache hit! simplifies to: T
[36570]:   rewriting LENGTH p = LENGTH q ∧ LENGTH p ≤ n ⇒ T with |- t ⇒ T ⇔ T
val it =
   Initial goal proved.
|- ∀p q n l. LENGTH p = LENGTH q ∧ LENGTH p ≤ n ⇒ LENGTH (cx l p q) ≤ n:
   proof





The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] CFP: Graphical Models for Security (GraMSec'16)

[Barbara Kordy]

*
GraMSec'16
The Third International Workshop on Graphical Models for Security
Co-located with CSF 2016

Lisbon, Portugal - June 27, 2016
http://gramsec.uni.lu/
*

Graphical security models provide an intuitive but systematic approach to
analyze security weaknesses of systems and to evaluate potential protection
measures. Formal methods and cyber security researchers, as well as 
security
professionals from industry and government, have proposed various graphical
security modeling schemes. Such models are used to capture different 
security
facets (digital, physical, and social) and address a range of challenges
including vulnerability assessment, risk analysis, defense analysis,
automated defensing, secure services composition, policy validation and
verification. The objective of the GraMSec workshop is to contribute to the
development of well-founded graphical security models, efficient algorithms
for their analysis, as well as methodologies for their practical usage.

The workshop seeks submissions from academia, industry, and government
presenting novel research on all theoretical and practical aspects of
graphical models for security. The topics of the workshop include, but are
not limited to:
- Graphical models for threat modeling and analysis
- Graphical models for risk analysis and management
- Graphical models for requirements analysis and management
- Textual and graphical representation for system, organizational, and 
business security
- Visual security modeling and analysis of socio-technical and 
cyber-physical systems
- Graphical security modeling for cyber situational awareness
- Graphical models supporting the security by design paradigm
- Methods for quantitative and qualitative analysis of graphical 
security models
- Formal semantics and verification of graphical security models
- Methods for (semi-)automatic generation of graphical security models
- Enhancement and/or optimization of existing graphical security models
- Scalable evaluation of graphical security models
- Evaluation algorithms for graphical security models
- Dynamic update of graphical security models
- Game theoretical approaches to graphical security modeling
- Attack trees, attack graphs and their variants
- Stochastic Petri nets, Markov chains, and Bayesian networks for security
- UML-based models and other graphical modeling approaches for security
- Software tools for graphical security modeling and analysis
- Case studies and experience reports on the use of graphical security 
modeling paradigm.

IMPORTANT DATES
Submission deadline: April 18, 2016
Acceptance notification: May 20, 2016
Camera ready version: June 3, 2016
GraMSec'16 workshop: June 27, 2016

SUBMISSION INSTRUCTIONS
We solicit two types of submissions:
- Regular papers (up to 15 pages) describing original and unpublished work
 within the scope of the workshop.
- Short papers (up to 7 pages) describing original and unpublished work in
 progress.

All submissions must be prepared using the LNCS style.

Each paper will undergo a thorough review process. All accepted (regular 
and
short) papers will be included in the workshop's post-proceedings. As last
year, we plan to publish the GraMSec'16 post-proceedings in the Lecture 
Notes
in Computer Science (LNCS) series of Springer (confirmation pending).
Submissions should be made using the GraMSec'16 EasyChair web site:
https://www.easychair.org/conferences/?conf=gramsec16.

INVITED SPEAKER
The invited lecture of GraMSec'16 will be given by Xinming Ou, associate
professor at Computer Science and Engineering, University of South 
Florida, USA

GENERAL CHAIR
Barbara Kordy, INSA Rennes, IRISA, France

PROGRAM COMMITTEE CO-CHAIRS
Mathias Ekstedt, KTH Royal Institute of Technology, Sweden
Dong Seong Kim, University of Canterbury, New Zealand

PROGRAM COMMITTEE
- Mathieu Acher, IRISA, FR
- Massimiliano Albanese, George Mason University, USA
- Ludovic Apvrille, Télécom ParisTech, CNRS LTCI, FR
- Thomas Bauereiss, DFKI GmbH, DE
- Giampaolo Bella, University of Catania, IT
- Stefano Bistarelli, University of Perugia, IT
- Marc Bouissou, EDF R, FR
- Frédéric Cuppens, Télécom Bretagne, FR
- Nora Cuppens-Boulahia, Télécom Bretagne, FR
- Binbin Chen, Advanced Digital Sciences Center, SG
- Jason Crampton, RHUL, UK
- Hervé Debar, Télécom SudParis, FR
- Giovanna Dondossola, RSE, IT
- Ulrik Franke, SICS, SE
- Frank Fransen, TNO, NL
- Olga Gadyatskaya, University of Luxembourg, LU
- Paolo Giorgini, University of Trento, IT
- Erlend Andreas Gjare, SINTEF, NO
- Dieter Gollmann, TU Hamburg, DE
- Olivier Heen, Technicolor, FR
- Hannes Holm, Swedish Defence Research Agency, SE
- Siv Hilde Houmb, Secure-NOK AS, NO
- René Rydhof Hansen, Aalborg University, DK
- Ravi Jhawar, University of Luxembourg, LU
- Henk Jonkers, BiZZdesign, NL
- Sushil Jajodia, George Mason University, USA
- Florian 

Re: [Hol-info] How to transform list format from "(cx l q p)" to "l"

[????]

Thank you for your reply!
 My version of HOL4 is HOL-4 [Kananaskis 10 (stdknl, built Mon Nov 10 14:27:30 
2014)], where Moscow ML version 2.01 (January 2004). Then from 
https://hol-theorem-prover.org/#get, I installed PolyML5.6-32bit, and pointed 
""bin/build". Then I got HOL-4 [Kananaskis 10 (stdknl, built Mon Feb 29 
21:47:05 2016)],where Moscow ML version 2.01 (January 2004). 
 I Opened HOL4, print"open listTheory;", I still can't use LENGTH_TAKE_EQ, it 
responed "Unbound value component: listTheory.LENGTH_TAKE_EQ". I had downloaded 
the files in https://github.com/HOL-Theorem-Prover/HOL. How to add it to HOL4's 
directory? After that ,I could print  "open listTheory;" in HOL4, and use 
LENGTH_TAKE_EQ.
  
 Thanks.
  
  

 

 -- Original --
  From:  "hol-info-request";;
 Date:  Wed, Mar 2, 2016 06:31 AM
 To:  "hol-info"; 
 
 Subject:  hol-info Digest, Vol 118, Issue 1

 

Send hol-info mailing list submissions to
hol-info@lists.sourceforge.net

To subscribe or unsubscribe via the World Wide Web, visit
https://lists.sourceforge.net/lists/listinfo/hol-info
or, via email, send a message with subject or body 'help' to
hol-info-requ...@lists.sourceforge.net

You can reach the person managing the list at
hol-info-ow...@lists.sourceforge.net

When replying, please edit your Subject line so it is more specific
than "Re: Contents of hol-info digest..."


Today's Topics:

   1. Re: How to transform list format from "(cx l q p)" to "l"
  (Anthony Fox)
   2. Re: Existential quantifier length (Michael Norrish)
   3. ? Summer School on Real-World Crypto and Privacy, June 5-10,
  Croatia (Veelasha)


--

Message: 1
Date: Mon, 29 Feb 2016 10:25:51 +
From: Anthony Fox 
Subject: Re: [Hol-info] How to transform list format from "(cx l q p)"
to "l"
To: ?? <956066...@qq.com>
Cc: hol-info 
Message-ID: <6c0cb742-6c45-45b0-80bd-78737f4cd...@cam.ac.uk>
Content-Type: text/plain; charset=utf-8

Which version of HOL4 are you using? The definitions of TAKE and DROP were 
altered in Jan 2008 (around about the time of kananaskis-5).

With the latest version of HOL4 Jeremy Dawson?s suggestion works fine for me. 
The proof seems to be trivial. (I?ve not tried it with older versions of HOL4.) 
How exactly did you define ?cx??

With

val cx_def = Define`
  (cx [] p q = p) /\
  (cx (h :: t) p q = TAKE h (cx t p q) ++ DROP h (cx t q p))`

we have

val th = Q.prove(
  `!p q l. (LENGTH p = LENGTH q) ==> (LENGTH (cx l p q) = LENGTH p)`,
  Induct_on `l` THEN RW_TAC list_ss [cx_def, listTheory.LENGTH_TAKE_EQ])

To get something closer to your definition of ?cx? I did

val cx_def = tDefine "cx" `
  (cx [] p q = p) /\
  (cx (h :: t) p q =
   TAKE (HD (h :: t)) (cx (TL (h :: t)) p q) ++
   DROP (HD (h :: t)) (cx (TL (h :: t)) q p))`
  (WF_REL_TAC `measure (\(x,y,z). LENGTH x)` THEN simp [])

but the proof worked without modification.

Regards,
Anthony

> On 29 Feb 2016, at 07:38, ?? <956066...@qq.com> wrote:
> 
> Hi,Jeremy
> Thank you for your reply!
> I tried. But it can't work.
> It responsed:
> - e (RW_TAC list_ss [LENGRH_DROP]);
> OK..
> Exception raised at Tactical.VALID:
> Invalid tactic
> ! Uncaught exception:
> ! HOL_ERR
> I think the reason is that the format of "(cx l q p)"  is not equal to "l", 
> though they are the same type "bool list".
> Thank you!
> 
> -- Original --
> From:  "hol-info-request";;
> Date:  Mon, Feb 29, 2016 01:08 PM
> To:  "hol-info";
> Subject:  hol-info Digest, Vol 117, Issue 9
> 
> Send hol-info mailing list submissions to
> hol-info@lists.sourceforge.net
> 
> To subscribe or unsubscribe via the World Wide Web, visit
> https://lists.sourceforge.net/lists/listinfo/hol-info
> or, via email, send a message with subject or body 'help' to
> hol-info-requ...@lists.sourceforge.net
> 
> You can reach the person managing the list at
> hol-info-ow...@lists.sourceforge.net
> 
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of hol-info digest..."
> 
> 
> Today's Topics:
> 
>1. How to transform list format from "(cx l q p)" to "l" ( Ada )
>2. Re: How to transform list format from "(cx l q p)" to "l"
>   (Jeremy Dawson)
>3. Two postdoc positions - Reasoning about concurrency and
>   distribution - Imperial College London (Petar Maksimovic)
> 
> 
> --
> 
> Message: 1
> Date: Sun, 28 Feb 2016 19:48:56 +0800
> From: " Ada " 
> Subject: [Hol-info] How to transform list format from "(cx l q p)" to
> "l"
> To: " hol-info " 
> Message-ID: 
> Content-Type: text/plain; charset="gb18030"

Re: [Hol-info] a question about rewrite in HOL4

[Ramana Kumar]

I think RW_TAC doesn't handle conditional rewrites very well. Try using rw
or simp instead.

This worked for me:

open listTheory

val cx_def = Define`
  (cx [] p q = p) ∧
  (cx (x::xs) p q =
  TAKE x (cx xs p q) ++
  DROP x (cx xs q p))`

val cx_length = Q.prove(
  `!l p q . (LENGTH p = LENGTH q) ==> (LENGTH (cx l p q) = LENGTH p)`,
  Induct \\ simp[cx_def,LENGTH_TAKE_EQ]);

val th = Q.prove(
  `!p q n l.
(LENGTH p = LENGTH q) /\ (LENGTH p <= n) ==>
  LENGTH (cx l p q) <= n `,
  simp[cx_length]);


On 5 March 2016 at 01:06, Ada  wrote:

> Hi,guys
> I am working with HOL4.
> I am going to prove
> g`!p q n l. ( (LENGTH p = LENGTH q) /\ (LENGTH p <= n)) ==> (LENGTH
> (cx l p q) <=n ) `;
> Where the definition of cx is
>
>   val cx_def = Define`
>   (cx [] p q = p) ∧
>   (cx (x::xs) p q =
>   TAKE x (cx xs p q) ++
>   DROP x (cx xs q p))`
>
> I had proved " !l p q . (LENGTH p = LENGTH q) ==> (LENGTH (cx l p q) =
> LENGTH p)", named "cx_length"
> so I used,
> e (RW_TAC list_ss [cx_length]);
> But it can't work, does anyone know the reason?
>
> Thanks!
>
>
> --
> 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=/4140
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] a question about rewrite in HOL4

[Ada]

Hi,guys
 I am working with HOL4. 
 I am going to prove
 g`!p q n l. ( (LENGTH p = LENGTH q) /\ (LENGTH p <= n)) ==> (LENGTH (cx l 
p q) <=n ) `;
 Where the definition of cx is 
val cx_def = Define`
   (cx [] p q = p) ??
   (cx (x::xs) p q =
   TAKE x (cx xs p q) ++
   DROP x (cx xs q p))`
  

 I had proved " !l p q . (LENGTH p = LENGTH q) ==> (LENGTH (cx l p q) = 
LENGTH p)", named "cx_length"
 so I used,
 e (RW_TAC list_ss [cx_length]);
 But it can't work, does anyone know the reason?
  
 Thanks!--
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=/4140___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] [VeryComp 2016] - 1st Call for Paper

[alexander . perucci]

[Apologies for multiple postings]

==  FIRST CALL FOR PAPERS ==

1st International Workshop on Formal to Practical Software Verification and 
Composition (VeryComp 2016)

Co-located event of STAF 2016 (http://staf2016.conf.tuwien.ac.at/) 
Wien, Austria - July 4th 2016

Web site: verycomp2016.disim.univaq.it

== IMPORTANT DATES ==

Paper submissions: April 18, 2016
Notification of authors: May 25, 2016
Camera-ready copies: June 20, 2016

== THEMES AND OBJECTIVES ==

Nowadays, modern applications are increasingly realized as distributed systems 
composing existing pieces of software that autonomically cooperates to achieve 
a common goal. As a matter of fact, this calls for new software composition 
paradigms, and patterns, modeling and verification methods that are practical 
and usable on one hand and formal on the other. Despite the great interest in 
practical Software Composition and Formal Verification in their isolation, no 
common and integrated approaches have been established yet. VeryComp promotes 
contributions related to the subject at different levels: from modelling and 
verification to analysis, from componentization to composition. Foundational 
contributions as well as concrete application experiments are sought.

VeryComp 2016 welcomes research papers, experience papers and tool 
presentations; nevertheless, papers describing novel research contributions and 
innovative applications are of particular interest. Details on workshop goals 
and themes can be found at: http://verycomp2016.disim.univaq.it

All accepted papers will be published as part of a Springer LNCS Proceedings 
Volume (Lecture Notes in Computer Science): http://www.springer.com/lncs

Furthermore, selected participants will be invited to submit an extended 
version of their papers after the workshop to a Thematic Series of the Springer 
JISA journal on Verification and Composition for the Internet of Services and 
Things (to appear soon on Springer).

Each submitted paper will undergo a formal peer review process by at least 3 PC 
members. Contributions can be:

- Regular papers (maximum 12 pages): In this category fall those contributions 
which propose novel research contributions, address challenging problems with 
innovative ideas, or offer practical contributions in the application of FM and 
SE approaches for building FI applications via software composition. Regular 
papers should clearly describe the situation or problem tackled, the relevant 
state of the art, the position or solution suggested and the potential benefits 
of the contribution.

- Short papers (maximum 8 pages): This category includes tool demonstrations, 
position papers, industrial experiences and case-studies, and visionary papers. 
Authors of papers reporting industrial experiences are encouraged to make their 
experimental results available for use by reviewers. Similarly, authors of tool 
demonstration papers should make their tool available for use by reviewers.


== Workshop Chairs ==

- Marco Autili, University of L’Aquila, Italy,
marco.aut...@univaq.it
- Massimo Tivoli, University of L’Aquila, Italy,
massimo.tiv...@univaq.it
- Luca Ferrucci, ISTI-CNR, Italy,
ferru...@isti.cnr.it
- Manuel Mazzara, Innopolis University, Russia,
m.mazz...@innopolis.ru
- Davide Bresolin, DISI - Universitu of Bologna, Italy,
davide.breso...@unibo.it
- Marcello Bersani, DEIB - Politecnico di Milano, Italy,
marcellomaria.bers...@polimi.it
- Marisol Garcia-Valls, University Carlos III, Spain,
mva...@it.uc3m.es

 == Program Committee ==
 
- Domenico Bianculli, Universitè du Luxembourg
- Stéphane Demri, NewYork University & CNRS, France
- Silvio Ghilardi, UniversitaΜ€ degli studi di Milano, Italy
- Nafees Qamar, Vanderbilt University, USA
- David Miguel Ramalho Pereira, Polytechnical School of Porto, Portugal
- Cesar Sanchez, IMDEA Software Institute, Spain
- Vincenzo Ciancia, ISTI-CNR, Italy
- Gwen Salaun, INRIA, Grenoble-Rhone-Alpes, France
- Guglielmo De Angelis, CNR-IASI/ISTI, Italy
- Paola Inverardi, University of L’Aquila, Italy
- Ivica Crnkovic, MaIardalen University, Sweden
- Radu Calinescu, University of York, UK
- Schahram Dustdar, University of Technology Wien, Austria
- Luciano Baresi, Politecnico di Milano, Italy
- Mauro Caporuscio, Linnaeus University, Sweden
- Nikolaos Georgantas, INRIA, France
- Salvatore Distefano, UniversitΓ  di Messina, Italy
- Victor Rivera, Innopolis University, Russia
- Pascal Poizat, Paris Ouest University and LIP6, France
- Saad Mubeen, MΓ€lardalen University, Sweden
- Hernan Melgratti, Universidad de Buenos Aires, Argentina
- Julio Medina, Universidad de Cantabria, Spain
- Patricia Lago, VU University Amsterdam, Nederland
- Carlo Ghezzi, Politecnico di Milano, Italy
- Antonio Bucchiarone, FBK-IRST, Italy
- Antonio Brogi, UniversitΓ  di Pisa, Italy
- Amel Bennaceur, The Open University, UK
- Carlo Bellettini, UniversitΓ  degli studi di Milano, Italy


== Web Chair & Publicity Chair ==

- Alexander Perucci, University