text:
ACSL By Example. Towards a Verified C Standard Library. Version for Frama-C Beryllium 2 April 2010
- Scot Spencer
- 2 years ago
- Views:
1 ACSL By Example Towards a Verified C Standard Library Version for Frama-C Beryllium 2 April 2010 Jochen Burghardt Jens Gerlach Kerstin Hartig Hans Pohl Juan Soto
2 This body of work was completed within the Device-Soft project 1, which is supported by the Programme Inter Carnot Fraunhofer from BMBF (Grant 01SF0804) and ANR. Except where otherwise noted, this work is licensed under 1 See 2
3 Foreword This report provides various examples for the formal specification, implementation, and deductive verification of C programs using the ANSI/ISO-C Specification Language (ACSL [1]) and the Jessie plug-in [2] of Frama-C [3]. We have chosen our examples from the C ++ Standard Library whose initial version is still known as the Standard Template Library (STL). 2 The STL contains a broad collection of generic algorithms that work not only on C-arrays but also on more elaborate containers, i.e., data structures. For the purposes of this document we have selected representative algorithms, and converted their implementation from C ++ function templates to ISO-C functions that work on arrays of type int. 3 In March 2009, while working in the context of the ES PASS 4 ITEA2 project, we released an initial version of this report. This earlier edition referred to the Lithium release of Frama-C. The report at hand is a completely revised and extended edition that refers to the Beryllium release of the Frama-C. We plan to extend this report in later releases by describing additional STL algorithms. Thus, step by step, this document will evolve from an ACSL tutorial to a report on a formally specified and deductively verified Standard Library for ANSI/ISO-C. Moreover, should ACSL be extended to a C ++ specification language, our work may be extended to a deductively verified C ++ Standard Library. You may comments, suggestions or errors to In particular, we encourage you to check vigilantly whether our formal specifications capture the essence of the informal description of the STL algorithms. We appreciate your feedback and hope that this document helps foster the adoption of deductive verification techniques. 2 See 3 We are not directly using int in the source code but rather value_type which is a typedef for int. 4 See 3
4 Contents 1. Introduction Acknowledgment Structure of this Document Types, Arrays, Ranges and Valid Indices Remarks on Jessie Automatic Theorem Provers The Hoare Calculus The Assignment Rule The Sequence Rule The Implication Rule The Choice Rule The Loop Rule Derived Rules Non-mutating Algorithms The equal Algorithm The mismatch Algorithm and equal again The find Algorithm The find Algorithm Reconsidered The find first of Algorithm The adjacent find Algorithm The max element Algorithm The max seq Algorithm The min element Algorithm The count Algorithm Mutating Algorithms The swap Algorithm The swap ranges Algorithm The fill Algorithm The copy Algorithm The replace copy Algorithm The remove copy Algorithm An Alternative Specification of the remove copy Algorithm The iota Algorithm Heap Operations Axiomatic Description of Heaps
5 5.2. The is heap Algorithm The push heap Algorithm The pop heap Algorithm The make heap Algorithm The sort heap Algorithm The Sorting Algorithm heap sort Results from Deductive Verification 105 A. Changes 107 A.1. New in Version (April 2010) A.2. New in Version (January 2010) A.3. Unofficial Release as part of the ES PASS project (March 2009) Bibliography 108 5
7 1. Introduction Frama-C [3] is a suite of software tools dedicated to the analysis of C source code. Frama-C development efforts are conducted and coordinated at CEA LIST[4], a laboratory of applied research on software-intensive technologies. Within Frama-C, the Jessie plug-in [2] enables deductive verification of C programs that have been annotated with the ANSI-C Specification Language (ACSL) [1]. ACSL can express a wide range of functional properties. The paramount notion in ACSL is the function contract. While many software engineering experts advocate the function contract mindset when designing complex software, they generally leave the actual expression of the contract to run-time assertions, or to comments in the source code. ACSL is expressly designed for writing the kind of properties that make up a function contract. [1] The Jessie plug-in uses Hoare-style weakest precondition computations to formally prove ACSL properties of a program fragment. Internally, Jessie relies on the languages and tools contained in the Why platform [5]. Verification conditions are generated and submitted to external automatic theorem provers or interactive proof assistants. We at Fraunhofer FIRST [6] see the great potential for deductive verification using ACSL. However, we recognize that for a novice there are challenges to overcome in order to effectively use the Jessie plug-in for deductive verification. In order to help users gain confidence, we have written this tutorial that demonstrates how to write annotations for existing C programs. This document provides several examples featuring a variety of annotated functions using ACSL. For an in-depth understanding of ACSL, we strongly recommend users to read the official Frama-C introductory tutorial [7] first. The principles presented in this paper are also documented in the ACSL reference document [8] Acknowledgment Many members from the Frama-C community provided valuable input and comments during the course of the development of this document. In particular, we wish to thank our partners from the Device-Soft 5 project, Pascal Cuoq, Virgile Prevosto and Benjamin Monate, as well as the Jessie developers, Claude Marché and Yannick Moy. 5 See 7
8 1.2. Structure of this Document The functions presented in this document were selected from the C ++ Standard Template Library (STL) [9]. The original C ++ implementation was stripped from its generic implementation and mapped to C-arrays of type value_type. Section 1.3 is devoted to commonly occurring statements that arise frequently throughout this tutorial, whereas Section 1.4 provides comments on the command-line options available in Frama-C and Jessie. Section 1.5 gives a short overview on the automatic theorem provers used for deductive verification. Chapter 2 provides a short introduction into the Hoare Calculus. Adhering to the classification used on the STL web-page [9], the examples in this tutorial were grouped as follows: non-mutating algorithms (discussed in Chapter 3) mutating algorithms (discussed in Chapter 4) heap operations (discussed in Chapter 5) Chapter 6 contains a summary of the results of the automatic theorem provers employed for the deductive verification of the aforementioned examples Types, Arrays, Ranges and Valid Indices In order to keep algorithms and specifications as general as possible, we use abstract type names on almost all occasions. We currently defined the following types: typedef int value_type; typedef int size_type; Programmers who know the types associated with STL containers will not be surprised that value_type refers to the type of values in an array whereas size_type will be used for the indices of an array. This approach allows one to modify e.g. an algorithm working on an int array to work on a char array by changing only one line of code, viz. the typedef of value_type. Moreover, we believe in better readability as it becomes clear whether a variable is used as an index or as a memory for a copy of an array element, just by looking at its type. Arrays and Ranges Many of the algorithms, described in the following sections, rely on common principles. In this section, we will list and explain their usage in finer detail. The C Standard describes an array as a contiguously allocated nonempty set of objects [10, ]. If n is a constant integer expression with a value greater than zero, then int a[n]; 8
9 describes an array of type int. In particular, for each i that is greater than or equal to 0 and less than n, we can dereference the pointer a+i. Let the following prototype represent a function, whose first argument is the address to a range and whose second argument is the length of this range. Valid Indices void example(value_type* a, size_type n); To be very precise, we have to use the term range instead of array. This is due to the fact, that functions may be called with empty ranges, i.e., with n == 0. Empty arrays, however, are not permitted according to the definition stated above. Nevertheless, we often use the term array and range interchangeably. The following ACSL fragment expresses the precondition that the function example expects that for each i, such that 0 <= i < n, the pointer a+i may be safely dereferenced. requires 0 <= n; requires \valid_range(a, 0, n-1); */ void example(value_type* a, size_type n); In this case we refer to each index i with 0 <= i < n as a valid index of a. ACSL s built-in predicate \valid_range(a, 0, n) refers to all addresses a+i where 0 <= i <= n. However, the array notation int a[n] of the C programming language refers only to the elements a+i where i satisfies 0 <= i < n. Users of ACSL must therefore specify \valid_range(a, 0, n-1). Introducing the following predicate based on the previous definition predicate is_valid_range(value_type* p, size_type n) = (0 <= n) && \valid_range(p, 0, n-1); */ we can shorten the specification of the function example to requires is_valid_range(a, n); */ void example(value_type* a, size_type n); The predicate is_valid_range will be frequently referenced in this document. 9
10 1.4. Remarks on Jessie Jessie is a plug-in that takes ACSL specified C-programs and performs deductive verification. Frama-C can be run using several Jessie options. The majority of the examples contained in this document were run with the following Frama-C command-line options: frama-c -jessie -jessie-no-regions filename The -jessie-no-regions option means that different pointers can point to the same region of memory. We chose to apply this option because it corresponds to the ISO-C Standard. By default Jessie assumes that different pointers point into different memory regions (see [11, Chapter 5]). Note, however, that some of the mutating algorithms in Chapter 4 require the Jessie default. We discuss the reasons for that in the particular sections on those algorithms. Another option to choose is the integer model. Jessie knows different integer models: exact, which means that C-integers are considered to behave as unbounded integers in the mathematical sense, i.e., ignoring the potential for an overflow. bounded, which does not consider integers in the mathematical sense, but rather machinedependent integers. Since overflows are detected using this integer model, one should select it, whenever one wishes to prevent overflow. modulo, which allows for overflow. If an overflow occurs, the value is taken modulo 2 n, where n is the number of bits of the specific type. Selection and invocation of a particular integer-model should be considered when generating verification conditions. This can be expressed using the following option: frama-c -jessie -jessie-int-model model filename By default, if no specific model is set, the bounded integer model is assumed for the generation of verification conditions. Note: All of the examples in this tutorial used the default integer model Automatic Theorem Provers Table 1.1 shows the five automatic theorem provers (ATP) used in conjunction with Jessie. Alt-Ergo is an automatic theorem prover dedicated to program verification developed at Laboratoire de Recherche en Informatique (LRI) [12]. Alt-Ergo is freely available, under the terms 10
11 Automatic Theorem Prover Version Alt-Ergo 0.9 Yices CVC3 1.5 Simplify Z3 2.1 Table 1.1.: Automatic theorem provers used during deductive verification of the CeCILL-C LICENSE. 6 CVC3 is an automatic theorem prover for Satisfiability Modulo Theories (SMT) problems [13]. It was developed at New York University (NYU) and there is essentially no limit on its use for research or commercial purposes. 7 Simplify is an automatic theorem prover [14]. The development of Simplify is not continued anymore. Nevertheless, it is still a highly efficient prover. As Chapter 6 demonstrates, Simplify is the only prover that could verify all generated proof obligations from this tutorial. Yices is an efficient SMT solver [15]. Z3 is a high-performance theorem prover developed at Microsoft Research [16]. A version for non-commercial use is also available. 8 6 For Details see and 7 See 8 See 11
13 2. The Hoare Calculus In 1969, C.A.R. Hoare introduced a calculus for formal reasoning about properties of imperative programs [17], which became known as Hoare Calculus. The basic notion is P Q R where P and R denote logical expressions and Q denotes a source-code fragment. Informally, this means If P holds before the execution of Q, then R will hold after the execution. Usually, P and R are called precondition and postcondition of Q, respectively. The syntax for logical expressions is described in [8, Section 2.2] in full detail. For the purposes of this tutorial, the notions shown in Table 2.1 are sufficient. Note that they closely resemble the logical and relational operators in C.!P negation P is not true P && Q conjunction P is true and Q is true P Q disjunction P is true or Q is true P ==> Q implication if P is true, then Q is true P <==> Q equivalence if, and only if, P is true, then Q is true x < y == z relation chain x is less than y and y is equal to z \forall int x; P(x) universal quantifier P(x) is true for every int value of x \exists int x; P(x) existential quantifier P(x) is true for some int value of x Table 2.1.: Some ACSL formula syntax x % 2 == 1 ++x; x % 2 == 0 (a) 0 <= x <= y ++x; 0 <= x <= y + 1 (b) true while (--x!= 0) sum += a[x]; x == 0 (c) Figure 2.1.: Example source-code fragments and annotations Figure 2.1 shows three example source-code fragments and annotations. Their informal meanings are as follows: (a) If x has an odd value before execution of the code ++x then x has an even value thereafter. 13
14 (b) If the value of x is in the range {0,..., y} before execution of the same code, then x s value is in the range {0,..., y + 1} after execution. (c) Under any circumstances, the value of x is zero after execution of the loop code. Any C programmer will confirm that these properties are valid. The examples were chosen to demonstrate also the following issues: For a given code fragment, there does not exist one fixed pre- or postcondition. Rather, the choice of formulas depends on the actual property to be verified, which comes from the application context. Examples (a) and (b) share the same code fragment, but have different pre- and postconditions. The postcondition need not be the most restricting possible formula that can be derived. In example (b), it is not an error that we stated only that 0 <= x although we know that even 1 <= x. In particular, pre- and postconditions need not contain all variables appearing in the code fragment. Neither sum nor a[] is referenced in the formulas of example (c). We can use the predicate true to denote the absence of a properly restricting precondition, as we did in example (c). It is not possible to express by pre- and postconditions that a given piece of code will always terminate. Example (c) only states that if the loop terminates, then x <= 0 will hold. In fact, if x has a negative value on entry, the loop will run forever. However, if the loop terminates, x == 0 will hold, and that is what example (c) claims. Usually, termination issues are dealt with separately from correctness issues. Termination proofs may, however, refer to properties stated (and verified) using the Hoare Calculus. Hoare provided the rules shown in Figures 2.2 to 2.10 in order to reason about programs. We will comment on them in the following sections The Assignment Rule We start with the rule that is probably the least intuitive of all Hoare-Calculus rules, viz. the assignment rule. This is depicted in Figure 2.2, where P {x e} denotes the result of substituting each occurrence of x in P by e. P {x --> e} x = e P Figure 2.2.: The assignment rule 14
15 For example, if P is 0 <= x <= 5 ==> a[2* x ] == 0, then P {x x+1} is 0 <=x+1<= 5 ==> a[2*(x+1)] == 0. Hence, we get Figure 2.3 as an example instance of the assignment rule. Note that parentheses are required in the index expression to get the correct 2*(x+1) rather than the faulty 2*x+1. x+1 > 0 && a[2*(x+1)] == 0 x = x+1 x > 0 && a[2*x] == 0 Figure 2.3.: An assignment rule example instance When first confronted with Hoare s assignment rule, most people are tempted to think of a simpler and more intuitive alternative, shown in Figure 2.4. Figures 2.5.(a) (c) show some example instances. P x = e P && x==e Figure 2.4.: Simpler, but faulty assignment rule y > 0 x = y+1 y>0 && x==y+1 true x = x+1 x==x+1 x < 0 x = 5 x<0 && x==5 (a) (b) (c) Figure 2.5.: Some example instances of the faulty rule from Figure 2.4 While (a) happens to be ok, (b) and (c) lead to postconditions that are obviously nonsensical formulas. The reason is that in the assignment in (b) the left-hand side variable x also appears in the right-hand side expression e, while the assignment in (c) just destroys the property from its precondition. Note that the correct example (a) can as well be obtained as an instance of the correct rule from Figure 2.2, since replacing x by y+1 in its postcondition yields y>0 && y+1 == y+1 as precondition, which is logically equivalent to just y>0. 15
16 2.2. The Sequence Rule The sequence rule, shown in Figure 2.6, combines two code fragments Q and S into a single one Q ; S. Note that the postcondition for Q must be identical to the precondition of S. This just reflects the sequential execution ( first do Q, then do S ) on a formal level. Thanks to this rule, we may annotate a program with interspersed formulas, as it is done in Frama-C. P Q R and R S T P Q ; S T Figure 2.6.: The sequence rule 2.3. The Implication Rule The implication rule, shown in Figure 2.7, allows us at any time to weaken a postcondition and to sharpen a precondition. We will provide application examples together with the next rule. P Q R P Q R if P ==> P and R ==> R Figure 2.7.: The implication rule 2.4. The Choice Rule The choice rule, depicted in Figure 2.8, is needed to verify if(...){...}else{...} statements. Both branches must establish the same postcondition, viz. S. The implication rule can be used to weaken differing postconditions S1 of a then branch and S2 of an else branch into a unified postcondition S1 S2, if necessary. In each branch, we may use what we know about the condition B, e.g. in the else branch, that it is false. If the else branch is missing, it can be considered as consisting of an empty sequence, having the postcondition P &&!B. Figure 2.9 shows an example application of the choice rule. The variable i may be used as an index into a ring buffer int a[n]. The shown code fragment just advances the index i appropriately. We verified that i remains a valid index into a[] provided it was valid before. Note the use of the implication rule to establish preconditions for the assignment rule as needed, and to unify the postconditions of the then and else branch, as required by the choice rule. 16
17 P && B Q S and P &&! B R S P if (B) { Q } else { R } S Figure 2.8.: The choice rule 0 <= i < n if (i < n - 1) { 0 <= i < n <= i + 1 < n i = i+1; 1 <= i < n 0 <= i < n } else { 0 <= i == n - 1 < n 0 == 0 && 0 < n i = 0; i == 0 && 0 < n 0 <= i < n } 0 <= i < n given precondition using that the condition i<n-1 holds in the then part by the implication rule by the assignment rule weakened by the implication rule using that then condition i<n-1 fails in the else part weakened by the implication rule by the assignment rule weakened by the implication rule by the choice rule from the then and the else part Figure 2.9.: An example application of the choice rule 2.5. The Loop Rule The loop rule, shown in Figure 2.10, is used to verify a while loop. This requires to find an appropriate formula, P, which is preserved by each execution of the loop body. P is also called a loop invariant. P && B S P P while (B) { S } B && P Figure 2.10.: The loop rule 17
18 To find it requires some intuition in many cases; for this reason, automatic theorem provers usually have problems with this task. As said above, the loop rule does not guarantee that the loop will always eventually terminate. It merely assures us that, if the loop has terminated, the postcondition holds. To emphasise this, the properties verifiable with the Hoare Calculus are usually called partial correctness properties, while properties that include program termination are called total correctness properties. As an example application, let us consider an abstract ring-buffer loop as shown in Figure < n given precondition 0 <= 0 < n follows trivially int i = 0; 0 <= i < n by the assignment rule while (!done) { 0 <= i < n &&!done may be assumed by the loop rule a[i] = getchar(); 0 <= i < n &&!done required property of getchar 0 <= i < n weakened by the implication rule if (i < n-1) i++; else i = 0; 0 <= i < n as seen above (Figure 2.9) process(a,i,&done); 0 <= i < n required property of process } 0 <= i < n by the loop rule Figure 2.11.: An abstract ring buffer loop Figure 2.11 shows a verification proof for the index i lying always within the valid range [0..n-1] during, and after, the loop. It uses the proof from Figure 2.9 as a sub-part. Note the following issues: To reuse the proof from Figure 2.9, we had to drop the conjunct!done, since we didn t consider it in Figure 2.9. In general, we may not infer P && S Q R && S from P Q R since the code fragment Q may just destroy the property S. This is obvious for Q being the fragment from Figure 2.9, and S being e.g. n!= 0. Suppose for a moment that process had been implemented in way such that it refuses to set done to true unless it is false at entry. In this case, we would really need that!done still holds after execution of Figure 2.9. We would have to do the proof again, looping-through an additional conjunct!done. We have similar problems to carry the property 0 <= i < n &&!done and 0 <= i < n over the statement a[i]=getchar() and process(a,i,&done), respectively. We need 18
19 to specify that neither getchar nor process is allowed to alter the value of i or n. In ACSL, there is a particular language construct assigns for that purpose, which is introduced in Section 4.1 on Page 54. In our example, the loop invariant can be established between any two statements of the loop body. However, this need not be the case in general. The loop rule only requires the invariant holds before the loop and at the end of the loop body. For example, process could well change the value of i 9 and even n intermediately, as long as it re-establishes the property 0 <= i < n immediately prior to returning. The loop invariant, 0 <= i < n, is established by the proof in Figure 2.9 also after termination of the loop. Thus, e.g., a final a[i]= \0 after the loop would be guaranteed not to lead to a bounds violation. Even if we would need the property 0 <= i < n to hold only immediately before the assignment a[i]=getchar(), since, e.g., process s body didn t use a or i, we would still have to establish 0 <= i < n as a loop invariant by the loop rule, since there is no other way to obtain any property inside a loop body. Apart from this formal reason it is obvious that 0 <= i < n wouldn t hold during the second loop iteration unless we reestablished it at the end of the first one, and that is just what the while rule requires Derived Rules The above rules don t cover all kinds of statements allowed in C. However, missing C-statements can be rewritten into a form that is semantically equivalent and covered by the Hoare rules. For example, switch (E) { case E1: Q1; break;... case En: Qn; break; default: Q0; break; } is semantically equivalent to if (E == E1) { Q1 } else... if (E == En) { Qn } else { Q0 } if E doesn t have side-effects. While the if-else form is usually slower in terms of execution speed on a real computer, this doesn t matter for verification purposes, which are separate from execution issues. 9 We would have to change the call to process(a,&i,&done) and the implementation of process appropriately. In this case we couldn t rely on the above-mentioned assigns clause for process. 19
20 Similarly, for (P; Q; R) { S } can be re-expressed as P; while (Q) { S ; R }, and so on. It is then possible to derive a Hoare rule for each kind of statement not previously discussed, by applying the classical rules to the corresponding re-expressed code fragment. However, we do not present these derived rules here. Although procedures cannot be re-expressed in the above way if they are (directly or mutually) recursive, it is still possible to derive Hoare rules for them. This requires the finding of appropriate procedure invariants similar to loop invariants. Non-recursive procedures can, of course, just be inlined to make the classical Hoare rules applicable. Note that goto cannot be rewritten in the above way; in fact, programs containing goto statements cannot be verified with the Hoare Calculus. See [18] for a similar calculus that can deal with arbitrary flowcharts, and hence arbitrary jumps. In fact, Hoare s work was based on that calculus. Later calculi inspired from Hoare s work have been designed to re-integrate support for arbitrary jumps. Jessie only supports forward jumps. However, in this tutorial, we will not discuss example programs containing a goto. 20
21 3. Non-mutating Algorithms In this chapter, we consider non-mutating algorithms, i.e., algorithms that neither change their arguments nor any objects outside their scope. This requirement can be formally expressed with the following assigns clause: assigns \nothing; Each algorithm in this chapter therefore uses this assigns clause in its specification. The specifications of these algorithms are not very complex. Nevertheless, we have tried to arrange them so that the earlier examples are simpler than the latter ones. All algorithms work on one-dimensional arrays ( ranges ). With one exception, the max seq function, all algorithms are also well-defined for empty ranges. Below are the six example algorithms we will discuss next. equal (Section 3.1 on Page 22) compares two ranges element by element. find (Section 3.3 on Page 30) provides sequential or linear search and returns the smallest index at which a given value occurs in a range. In Section 3.4, on Page 33, a predicate is introduced in order to simplify the specification. find first of (Section 3.5, on Page 36) provides similar to find a sequential search, but unlike find it does not search for a particular value, but for the least index of a given range which occurs in another range. adjacent find which can be used to find equal neighbours in an array (Section 3.6). max element (Section 3.7, on Page 42) returns an index to a maximum element in range. Similar to find it also returns the smallest of all possible indices. max seq (Section 3.8, on Page 46) is very similar to max element and will serve as an example of modular verification. It returns the maximum value itself rather than an index to it. min element which can be used to find the smallest element in an array (Section 3.9). count (Section 3.10, on Page 50) returns the number of occurrences of a given value in a range. Here we will employ some user-defined axioms to formally specify count. 21
22 3.1. The equal Algorithm The equal algorithm in the C ++ Standard Library compares two generic sequences. For our purposes we have modified the generic implementation 10 to that of an array of type size_type. The signature now reads: bool equal(const value_type* a, int n, const value_type* b); The function returns 1 if for the two sequences a[0] == b[0] a[1] == b[1]... a[n-1] == b[n-1] holds. Otherwise, equal returns Formal Specification of equal The ACSL specification of equal is shown in Listing requires is_valid_range(a, n); 3 requires is_valid_range(b, n); 4 5 assigns \nothing; 6 7 behavior all_equal: 8 assumes \forall size_type i; 0 <= i < n ==> a[i] == b[i]; 9 ensures \result == 1; behavior some_not_equal: 12 assumes \exists size_type i; 0 <= i < n && a[i]!= b[i]; 13 ensures \result == 0; complete behaviors all_equal, some_not_equal; 16 disjoint behaviors all_equal, some_not_equal; 17 */ 18 bool equal(const value_type* a, size_type n, const value_type* b); Listing 3.1: Formal specification of equal Lines 2 and 3 in Listing 3.1 formalise the requirements that n is non-negative and that the pointers a and b point to n contiguously allocated objects of type value_type (see also Section 1.3). 10 See 22
Applications of formal verification for secure Cloud environments at CEA LIST
Applications of formal verification for secure Cloud environments at CEA LIST Nikolai Kosmatov joint work with A.Blanchard, F.Bobot, M.Lemerre,... SEC2, Lille, June 30 th, 2015 N. Kosmatov (CEA LIST) FormalMore information
CHAPTER 7 GENERAL PROOF SYSTEMS 1 Introduction Proof systems are built to prove statements. They can be thought as an inference machine with special statements, called provable statements, or sometimesMore information
Rigorous. Development. Software. Program Verification. & Springer. An Introduction to. Jorge Sousa Pinto. Jose Bacelar Almeida Maria Joao Frade
Jose Bacelar Almeida Maria Joao Frade Jorge Sousa Pinto Simao Melo de Sousa Rigorous Software Development An Introduction to Program Verification & Springer Contents 1 Introduction 1 1.1 A Formal ApproachMore information
Constructing Contracts: Making Discrete Mathematics Relevant to Beginning Programmers
Constructing Contracts: Making Discrete Mathematics Relevant to Beginning Programmers TIMOTHY S. GEGG-HARRISON Winona State University Although computer scientists understand the importance of discreteMore information
FROM SAFETY TO SECURITY SOFTWARE ASSESSMENTS AND GUARANTEES FLORENT KIRCHNER (LIST) M loc 12 ONBOARD SOFTWARE SIZE 10 Volt (2011) F-35 (2012) 8 6 787 (2010) F-35 (2010) 4 2 F-22 (2005) 0 WHY DO WE TRUSTMore information
Rigorous Software Development CSCI-GA 3033-009
Rigorous Software Development CSCI-GA 3033-009 Instructor: Thomas Wies Spring 2013 Lecture 11 Semantics of Programming Languages Denotational Semantics Meaning of a program is defined as the mathematicalMore information
Chair of Software Engineering. Software Verification. Assertion Inference. Carlo A. Furia
Chair of Software Engineering Software Verification Assertion Inference Carlo A. Furia Proving Programs Automatically The Program Verification problem: Given: a program P and a specification S = [Pre,More information
Rigorous Software Engineering Hoare Logic and Design by Contracts
Rigorous Software Engineering Hoare Logic and Design by Contracts Simão Melo de Sousa RELEASE (UBI), LIACC (Porto) Computer Science Department University of Beira Interior, Portugal 2010-2011 S. Melo deMore information
A Framework for the Semantics of Behavioral Contracts
A Framework for the Semantics of Behavioral Contracts Ashley McNeile Metamaxim Ltd, 48 Brunswick Gardens, London W8 4AN, UK email@example.com Abstract. Contracts have proved a powerful conceptMore information
Lecture Notes on Linear Search
Lecture Notes on Linear Search 15-122: Principles of Imperative Computation Frank Pfenning Lecture 5 January 29, 2013 1 Introduction One of the fundamental and recurring problems in computer science isMore information
Automated Theorem Proving - summary of lecture 1
Automated Theorem Proving - summary of lecture 1 1 Introduction Automated Theorem Proving (ATP) deals with the development of computer programs that show that some statement is a logical consequence ofMore information
3. Mathematical Induction
3. MATHEMATICAL INDUCTION 83 3. Mathematical Induction 3.1. First Principle of Mathematical Induction. Let P (n) be a predicate with domain of discourse (over) the natural numbers N = {0, 1,,...}. If (1)More information
Automated Program Behavior Analysis
Automated Program Behavior Analysis Stacy Prowell firstname.lastname@example.com March 2005 SQRL / SEI Motivation: Semantics Development: Most engineering designs are subjected to extensive analysis; software isMore information
What's Wrong With Formal Programming Methods? Eric C.R. Hehner
What's Wrong With Formal Programming Methods? Eric C.R. Hehner Department of Computer Science, University of Toronto, Toronto M5S 1A4 Canada The January 1991 issue of Computing Research News includes theMore information
[Refer Slide Time: 05:10]
Principles of Programming Languages Prof: S. Arun Kumar Department of Computer Science and Engineering Indian Institute of Technology Delhi Lecture no 7 Lecture Title: Syntactic Classes Welcome to lectureMore information
InvGen: An Efficient Invariant Generator
InvGen: An Efficient Invariant Generator Ashutosh Gupta and Andrey Rybalchenko Max Planck Institute for Software Systems (MPI-SWS) Abstract. In this paper we present InvGen, an automatic linear arithmeticMore information
Bounded Cost Algorithms for Multivalued Consensus Using Binary Consensus Instances
Bounded Cost Algorithms for Multivalued Consensus Using Binary Consensus Instances Jialin Zhang Tsinghua University firstname.lastname@example.com Wei Chen Microsoft Research Asia email@example.com AbstractMore information
Computer Arithmetic Aliasing issues: Call by reference, Pointer programs
Computer Arithmetic Aliasing issues: Call by reference, Pointer programs Claude Marché Cours MPRI 2-36-1 Preuve de Programme 24 janvier 2014 Outline Exercises from last lecture Computer Arithmetic HandlingMore information
International Journal of Computer ScienceandCommunication Vol. 2, No. 1, January-June2011, pp. 153-157 PROPERTECHNIQUEOFSOFTWARE INSPECTIONUSING GUARDED COMMANDLANGUAGE Neeraj Kumar Singhania University,More information
LEVERAGING DEDUCTIVE VERIFICATION IN INDUSTRIAL CONTEXTS CEA S SOFTWARE SAFETY LABORATORY 1995: LEAP FROM DYNAMIC TO STATIC CODE ANALYSIS! CAVEAT: ARCHITECTURE C source code VC Generator Formal specificationsMore information
Formal Languages and Automata Theory - Regular Expressions and Finite Automata -
Formal Languages and Automata Theory - Regular Expressions and Finite Automata - Samarjit Chakraborty Computer Engineering and Networks Laboratory Swiss Federal Institute of Technology (ETH) Zürich MarchMore information
Regression Verification: Status Report
Regression Verification: Status Report Presentation by Dennis Felsing within the Projektgruppe Formale Methoden der Softwareentwicklung 2013-12-11 1/22 Introduction How to prevent regressions in softwareMore information
3 Extending the Refinement Calculus
Building BSP Programs Using the Refinement Calculus D.B. Skillicorn? Department of Computing and Information Science Queen s University, Kingston, Canada email@example.com Abstract. We extend theMore information
Mathematics for Computer Science/Software Engineering. Notes for the course MSM1F3 Dr. R. A. Wilson
Mathematics for Computer Science/Software Engineering Notes for the course MSM1F3 Dr. R. A. Wilson October 1996 Chapter 1 Logic Lecture no. 1. We introduce the concept of a proposition, which is a statementMore information
Chapter II. Controlling Cars on a Bridge
Chapter II. Controlling Cars on a Bridge 1 Introduction The intent of this chapter is to introduce a complete example of a small system development. During this development, you will be made aware of theMore information
Chapter 1: Key Concepts of Programming and Software Engineering
Chapter 1: Key Concepts of Programming and Software Engineering Software Engineering Coding without a solution design increases debugging time - known fact! A team of programmers for a large software developmentMore information
The programming language C. sws1 1
The programming language C sws1 1 The programming language C invented by Dennis Ritchie in early 1970s who used it to write the first Hello World program C was used to write UNIX Standardised as K&C (KernighanMore information
A simple algorithm with no simple verication
A simple algorithm with no simple verication Laszlo Csirmaz Central European University Abstract The correctness of a simple sorting algorithm is resented, which algorithm is \evidently wrong" at the rstMore information
Induction. Margaret M. Fleck. 10 October These notes cover mathematical induction and recursive definition
Induction Margaret M. Fleck 10 October 011 These notes cover mathematical induction and recursive definition 1 Introduction to induction At the start of the term, we saw the following formula for computingMore information
Specification and Analysis of Contracts Lecture 1 Introduction
Specification and Analysis of Contracts Lecture 1 Introduction Gerardo Schneider firstname.lastname@example.com http://folk.uio.no/gerardo/ Department of Informatics, University of Oslo SEFM School, Oct. 27 - Nov.More information
WHAT ARE MATHEMATICAL PROOFS AND WHY THEY ARE IMPORTANT? introduction Many students seem to have trouble with the notion of a mathematical proof. People that come to a course like Math 216, who certainlyMore information
Why? A central concept in Computer Science. Algorithms are ubiquitous.
Analysis of Algorithms: A Brief Introduction Why? A central concept in Computer Science. Algorithms are ubiquitous. Using the Internet (sending email, transferring files, use of search engines, onlineMore information
Data Structure with C
Subject: Data Structure with C Topic : Tree Tree A tree is a set of nodes that either:is empty or has a designated node, called the root, from which hierarchically descend zero or more subtrees, whichMore information
6 EXTENDING ALGEBRA. 6.0 Introduction. 6.1 The cubic equation. Objectives
6 EXTENDING ALGEBRA Chapter 6 Extending Algebra Objectives After studying this chapter you should understand techniques whereby equations of cubic degree and higher can be solved; be able to factoriseMore information
1 INTRODUCTION 1.1 What is a Programming Language? 1.2 Abstractions in Programming Languages 1.3 Computational Paradigms 1.4 Language Definition 1.5 Language Translation 1.6 Language Design How we communicateMore information
Formal Verification of Software
Formal Verification of Software Sabine Broda Department of Computer Science/FCUP 12 de Novembro de 2014 Sabine Broda (DCC-FCUP) Formal Verification of Software 12 de Novembro de 2014 1 / 26 Formal VerificationMore information
Extended Static Checking for Java
Lukas TU München - Seminar Verification 14. Juli 2011 Outline 1 Motivation 2 ESC/Java example 3 ESC/JAVA architecture VC generator Simplify 4 JML + ESC/Java annotation language JML What ESC/Java checksMore information
Virtual Time and Timeout in Client-Server Networks
Virtual Time and Timeout in Client-Server Networks Jayadev Misra July 13, 2011 Contents 1 Introduction 2 1.1 Background.............................. 2 1.1.1 Causal Model of Virtual Time...............More information
StaRVOOrS: A Tool for Combined Static and Runtime Verification of Java
StaRVOOrS: A Tool for Combined Static and Runtime Verification of Java Jesús Mauricio Chimento 1, Wolfgang Ahrendt 1, Gordon J. Pace 2, and Gerardo Schneider 3 1 Chalmers University of Technology, Sweden.More information
Overview Motivating Examples Interleaving Model Semantics of Correctness Testing, Debugging, and Verification
Introduction Overview Motivating Examples Interleaving Model Semantics of Correctness Testing, Debugging, and Verification Advanced Topics in Software Engineering 1 Concurrent Programs Characterized byMore information
Elementary Number Theory We begin with a bit of elementary number theory, which is concerned
CONSTRUCTION OF THE FINITE FIELDS Z p S. R. DOTY Elementary Number Theory We begin with a bit of elementary number theory, which is concerned solely with questions about the set of integers Z = {0, ±1,More information
Software Engineering Techniques
Software Engineering Techniques Low level design issues for programming-in-the-large. Software Quality Design by contract Pre- and post conditions Class invariants Ten do Ten do nots Another type of summaryMore information
Scalable Automated Symbolic Analysis of Administrative Role-Based Access Control Policies by SMT solving
Scalable Automated Symbolic Analysis of Administrative Role-Based Access Control Policies by SMT solving Alessandro Armando 1,2 and Silvio Ranise 2, 1 DIST, Università degli Studi di Genova, Italia 2 SecurityMore information
A simple criterion on degree sequences of graphs
Discrete Applied Mathematics 156 (2008) 3513 3517 Contents lists available at ScienceDirect Discrete Applied Mathematics journal homepage: www.elsevier.com/locate/dam Note A simple criterion on degreeMore information
Structure of Presentation. Stages in Teaching Formal Methods. Motivation (1) Motivation (2) The Scope of Formal Methods (1)
Stages in Teaching Formal Methods A. J. Cowling Structure of Presentation Introduction to Issues Motivation for this work. Analysis of the Role of Formal Methods Define their scope; Review their treatmentMore information
Introducing Formal Methods. Software Engineering and Formal Methods
Introducing Formal Methods Formal Methods for Software Specification and Analysis: An Overview 1 Software Engineering and Formal Methods Every Software engineering methodology is based on a recommendedMore information
Dedekind s forgotten axiom and why we should teach it (and why we shouldn t teach mathematical induction in our calculus classes)
Dedekind s forgotten axiom and why we should teach it (and why we shouldn t teach mathematical induction in our calculus classes) by Jim Propp (UMass Lowell) March 14, 2010 1 / 29 Completeness Three commonMore information
Verification of Imperative Programs in Theorema
Verification of Imperative Programs in Theorema Laura Ildikó Kovács, Nikolaj Popov, Tudor Jebelean 1 Research Institute for Symbolic Computation, Johannes Kepler University, A-4040 Linz, Austria InstituteMore information
2. Methods of Proof Types of Proofs. Suppose we wish to prove an implication p q. Here are some strategies we have available to try.
2. METHODS OF PROOF 69 2. Methods of Proof 2.1. Types of Proofs. Suppose we wish to prove an implication p q. Here are some strategies we have available to try. Trivial Proof: If we know q is true thenMore information
Boogie: A Modular Reusable Verifier for Object-Oriented Programs
Boogie: A Modular Reusable Verifier for Object-Oriented Programs M. Barnett, B.E. Chang, R. DeLine, B. Jacobs, K.R.M. Leino Lorenzo Baesso ETH Zurich Motivation Abstract Domains Modular Architecture AutomaticMore information
Introduction to Diophantine Equations
Introduction to Diophantine Equations Tom Davis firstname.lastname@example.com http://www.geometer.org/mathcircles September, 2006 Abstract In this article we will only touch on a few tiny parts of the fieldMore information
Introduction to Static Analysis for Assurance
Introduction to Static Analysis for Assurance John Rushby Computer Science Laboratory SRI International Menlo Park CA USA John Rushby Static Analysis for Assurance: 1 Overview What is static analysis?More information
The last three chapters introduced three major proof techniques: direct,
CHAPTER 7 Proving Non-Conditional Statements The last three chapters introduced three major proof techniques: direct, contrapositive and contradiction. These three techniques are used to prove statementsMore information
The Trip Scheduling Problem
The Trip Scheduling Problem Claudia Archetti Department of Quantitative Methods, University of Brescia Contrada Santa Chiara 50, 25122 Brescia, Italy Martin Savelsbergh School of Industrial and SystemsMore information
Interactive Software Verification
Interactive Software Verification Spring Term 2013 Holger Gast email@example.com 25.6.2013 1 H.Gast firstname.lastname@example.com Interactive Software Verification, 25.6.2013 Today Manipulating lists on the heap GhostMore information
6. Control Structures
- 35 - Control Structures: 6. Control Structures A program is usually not limited to a linear sequence of instructions. During its process it may bifurcate, repeat code or take decisions. For that purpose,More information
Object Oriented Software Design
Object Oriented Software Design Introduction to Java - II Giuseppe Lipari http://retis.sssup.it/~lipari Scuola Superiore Sant Anna Pisa October 28, 2010 G. Lipari (Scuola Superiore Sant Anna) IntroductionMore information
Some Polynomial Theorems. John Kennedy Mathematics Department Santa Monica College 1900 Pico Blvd. Santa Monica, CA 90405 firstname.lastname@example.com.
Some Polynomial Theorems by John Kennedy Mathematics Department Santa Monica College 1900 Pico Blvd. Santa Monica, CA 90405 email@example.com This paper contains a collection of 31 theorems, lemmas,More information
Software Testing & Analysis (F22ST3): Static Analysis Techniques 2. Andrew Ireland
Software Testing & Analysis (F22ST3) Static Analysis Techniques Andrew Ireland School of Mathematical and Computer Science Heriot-Watt University Edinburgh Software Testing & Analysis (F22ST3): StaticMore information
Regular Languages and Finite Automata
Regular Languages and Finite Automata 1 Introduction Hing Leung Department of Computer Science New Mexico State University Sep 16, 2010 In 1943, McCulloch and Pitts [4] published a pioneering work on aMore information
C++ Programming Language
C++ Programming Language Lecturer: Yuri Nefedov 7th and 8th semesters Lectures: 34 hours (7th semester); 32 hours (8th semester). Seminars: 34 hours (7th semester); 32 hours (8th semester). Course abstractMore information
The Classes P and NP
The Classes P and NP We now shift gears slightly and restrict our attention to the examination of two families of problems which are very important to computer scientists. These families constitute theMore information
M.Sc. program in mathematics INTRODUCTORY SET THEORY Katalin Károlyi Department of Applied Analysis, Eötvös Loránd University H-1088 Budapest, Múzeum krt. 6-8. CONTENTS 1. SETS Set, equal sets, subset,More information
MPLAB TM C30 Managed PSV Pointers. Beta support included with MPLAB C30 V3.00
MPLAB TM C30 Managed PSV Pointers Beta support included with MPLAB C30 V3.00 Contents 1 Overview 2 1.1 Why Beta?.............................. 2 1.2 Other Sources of Reference..................... 2 2More information
2) Write in detail the issues in the design of code generator.
COMPUTER SCIENCE AND ENGINEERING VI SEM CSE Principles of Compiler Design Unit-IV Question and answers UNIT IV CODE GENERATION 9 Issues in the design of code generator The target machine Runtime StorageMore information
The Foundations: Logic and Proofs. Chapter 1, Part III: Proofs
The Foundations: Logic and Proofs Chapter 1, Part III: Proofs Rules of Inference Section 1.6 Section Summary Valid Arguments Inference Rules for Propositional Logic Using Rules of Inference to Build ArgumentsMore information
EMBEDDING COUNTABLE PARTIAL ORDERINGS IN THE ENUMERATION DEGREES AND THE ω-enumeration DEGREES MARIYA I. SOSKOVA AND IVAN N. SOSKOV 1. Introduction One of the most basic measures of the complexity of aMore information
Integrating Benders decomposition within Constraint Programming
Integrating Benders decomposition within Constraint Programming Hadrien Cambazard, Narendra Jussien email: {hcambaza,email@example.com École des Mines de Nantes, LINA CNRS FRE 2729 4 rue Alfred Kastler BPMore information
TOPOLOGY: THE JOURNEY INTO SEPARATION AXIOMS VIPUL NAIK Abstract. In this journey, we are going to explore the so called separation axioms in greater detail. We shall try to understand how these axiomsMore information
Coverability for Parallel Programs
2015 http://excel.fit.vutbr.cz Coverability for Parallel Programs Lenka Turoňová* Abstract We improve existing method for the automatic verification of systems with parallel running processes. The techniqueMore information
Runtime Verification of Computer Programs and its Application in Programming Education
Runtime Verification of Computer Programs its Application in Programming Education Magdalina V. Todorova, Petar R. Armyanov Abstract The paper presents a technique for runtime program verification itsMore information
Object Oriented Software Design
Object Oriented Software Design Introduction to Java - II Giuseppe Lipari http://retis.sssup.it/~lipari Scuola Superiore Sant Anna Pisa September 14, 2011 G. Lipari (Scuola Superiore Sant Anna) IntroductionMore information
Chapter 7: Functional Programming Languages
Chapter 7: Functional Programming Languages Aarne Ranta Slides for the book Implementing Programming Languages. An Introduction to Compilers and Interpreters, College Publications, 2012. Fun: a languageMore information
NODAL ANALYSIS. Circuits Nodal Analysis 1 M H Miller
NODAL ANALYSIS A branch of an electric circuit is a connection between two points in the circuit. In general a simple wire connection, i.e., a 'short-circuit', is not considered a branch since it is knownMore information
Theorem (informal statement): There are no extendible methods in David Chalmers s sense unless P = NP.
Theorem (informal statement): There are no extendible methods in David Chalmers s sense unless P = NP. Explication: In his paper, The Singularity: A philosophical analysis, David Chalmers defines an extendibleMore information
Formal Verification Coverage: Computing the Coverage Gap between Temporal Specifications
Formal Verification Coverage: Computing the Coverage Gap between Temporal Specifications Sayantan Das Prasenjit Basu Ansuman Banerjee Pallab Dasgupta P.P. Chakrabarti Department of Computer Science & EngineeringMore information
Chapter 4 Software Lifecycle and Performance Analysis
Chapter 4 Software Lifecycle and Performance Analysis This chapter is aimed at illustrating performance modeling and analysis issues within the software lifecycle. After having introduced software andMore information
CONTENTS 1. Peter Kahn. Spring 2007
CONTENTS 1 MATH 304: CONSTRUCTING THE REAL NUMBERS Peter Kahn Spring 2007 Contents 2 The Integers 1 2.1 The basic construction.......................... 1 2.2 Adding integers..............................More information
ACADEMIC YEAR: 0 7 VALLIAMMAI ENGINEERING COLLEGE SRM NAGAR, KATTANKULATHUR 0 0 SEMESTER: ODD BRANCH: MCA YEAR: I SEMESTER: I SUBJECT CODE AND NAME: MC70 Problem Solving and Programming NAME OF THE FACULTYMore information
Chapter 5. Selection 5-1
Chapter 5 Selection 5-1 Selection (Decision) The second control logic structure is selection: Selection Choosing between two or more alternative actions. Selection statements alter the sequential flowMore information
Decision Logic: if, if else, switch, Boolean conditions and variables
CS 1044 roject 3 Fall 2009 Decision Logic: if, if else, switch, Boolean conditions and variables This programming assignment uses many of the ideas presented in sections 3 through 5 of the Dale/Weems textMore information
SJÄLVSTÄNDIGA ARBETEN I MATEMATIK MATEMATISKA INSTITUTIONEN, STOCKHOLMS UNIVERSITET Automated Theorem Proving av Tom Everitt 2010 - No 8 MATEMATISKA INSTITUTIONEN, STOCKHOLMS UNIVERSITET, 106 91 STOCKHOLMMore information
Chapter 4, Arithmetic in F [x] Polynomial arithmetic and the division algorithm.
Chapter 4, Arithmetic in F [x] Polynomial arithmetic and the division algorithm. We begin by defining the ring of polynomials with coefficients in a ring R. After some preliminary results, we specializeMore information
Sequential Data Structures
Sequential Data Structures In this lecture we introduce the basic data structures for storing sequences of objects. These data structures are based on arrays and linked lists, which you met in first yearMore information
Mathematical Induction
Mathematical Induction In logic, we often want to prove that every member of an infinite set has some feature. E.g., we would like to show: N 1 : is a number 1 : has the feature Φ ( x)(n 1 x! 1 x) HowMore information
Towards practical reactive security audit using extended static checkers 1
Towards practical reactive security audit using extended static checkers 1 Julien Vanegue 1 Shuvendu K. Lahiri 2 1 Bloomberg LP, New York 2 Microsoft Research, Redmond May 20, 2013 1 The work was conductedMore information
The Union-Find Problem Kruskal s algorithm for finding an MST presented us with a problem in data-structure design. As we looked at each edge,
The Union-Find Problem Kruskal s algorithm for finding an MST presented us with a problem in data-structure design. As we looked at each edge, cheapest first, we had to determine whether its two endpointsMore information
4. CLASSES OF RINGS 4.1. Classes of Rings class operator A-closed Example 1: product Example 2:
4. CLASSES OF RINGS 4.1. Classes of Rings Normally we associate, with any property, a set of objects that satisfy that property. But problems can arise when we allow sets to be elements of larger setsMore information
Notes on Factoring. MA 206 Kurt Bryan
The General Approach Notes on Factoring MA 26 Kurt Bryan Suppose I hand you n, a 2 digit integer and tell you that n is composite, with smallest prime factor around 5 digits. Finding a nontrivial factorMore information
Cost Model: Work, Span and Parallelism. 1 The RAM model for sequential computation:
CSE341T 08/31/2015 Lecture 3 Cost Model: Work, Span and Parallelism In this lecture, we will look at how one analyze a parallel program written using Cilk Plus. When we analyze the cost of an algorithmMore information
16.1 MAPREDUCE. For personal use only, not for distribution. 333
For personal use only, not for distribution. 333 16.1 MAPREDUCE Initially designed by the Google labs and used internally by Google, the MAPREDUCE distributed programming model is now promoted by severalMore information
Fundamental Computer Science Concepts Sequence TCSU CSCI SEQ A
Fundamental Computer Science Concepts Sequence TCSU CSCI SEQ A A. Description Introduction to the discipline of computer science; covers the material traditionally found in courses that introduce problemMore information
5 =5. Since 5 > 0 Since 4 7 < 0 Since 0 0
a p p e n d i x e ABSOLUTE VALUE ABSOLUTE VALUE E.1 definition. The absolute value or magnitude of a real number a is denoted by a and is defined by { a if a 0 a = a if aMore information
A Case Study on Verification of a Cloud Hypervisor by Proof and Structural Testing
A Case Study on Verification of a Cloud Hypervisor by Proof and Structural Testing Nikolai Kosmatov 1, Matthieu Lemerre 1, and Céline Alec 2 1 CEA, LIST, Software Reliability Laboratory, PC 174, 91191More information
Lecture 3: Finding integer solutions to systems of linear equations
Lecture 3: Finding integer solutions to systems of linear equations Algorithmic Number Theory (Fall 2014) Rutgers University Swastik Kopparty Scribe: Abhishek Bhrushundi 1 Overview The goal of this lectureMore information
A Propositional Dynamic Logic for CCS Programs
A Propositional Dynamic Logic for CCS Programs Mario R. F. Benevides and L. Menasché Schechter {mario,email@example.com Abstract This work presents a Propositional Dynamic Logic in which the programs areMore information
Tool-Assisted Unit-Test Generation and Selection Based on Operational Abstractions
Tool-Assisted Unit-Test Generation and Selection Based on Operational Abstractions Tao Xie 1 and David Notkin 2 (email@example.com,firstname.lastname@example.com) 1 Department of Computer Science, North CarolinaMore information
VDM vs. Programming Language Extensions or their Integration
VDM vs. Programming Language Extensions or their Integration Alexander A. Koptelov and Alexander K. Petrenko Institute for System Programming of Russian Academy of Sciences (ISPRAS), B. Communisticheskaya,More information
Iteration, Induction, and Recursion
CHAPTER 2 Iteration, Induction, and Recursion The power of computers comes from their ability to execute the same task, or different versions of the same task, repeatedly. In computing, the theme of iterationMore information
Name: Class: Date: 9. The compiler ignores all comments they are there strictly for the convenience of anyone reading the program.
Name: Class: Date: Exam #1 - Prep True/False Indicate whether the statement is true or false. 1. Programming is the process of writing a computer program in a language that the computer can respond toMore information


text:
When I first looked into this company I wasn't sure about them but I can honestly say that taking the risk and going for it has really helped a lot. Smile direct club has been very precise with me and has had outstanding customer service overall. A little more than four weeks ago I had taken my impressions and the first set came back rejected so I had to do a retake which was going to cost me an additional $49 but at that point I decided not to do it because I couldn't afford to pay extra for the retake kit so I contacted them via chat online and they sent me a new kit free of charge. Once the new kit arrived I did the retake and Guess What!... Success! So last Wednesday I was informed that I was selected to move forward based on my impressions and that I would receive my treatment plan for review within seven to ten business days. Today is Monday the first and I was contacted via email last Wednesday so it took them only five days to create my plan. I am so excited and look forward to the results of my progress. I have read previous reviews that others didn't find the program to go to well with them but for me so far things are going smoothly I receive my first set of aligners withing three weeks and I couldn't be happier overall this process took about four weeks and that's only because I had to do a retake of impressions but they are really amazing and anyone who wants an awesome smile at an affordable cost should consider them because it is worth the try.
Smile Direct Club
When I first looked into this company I wasn't...
Smile Direct Club Update
So yesterday I received an email from smile Direct club stating that they were in the process of thermoforming my aligners. I'm not sure what the next process is afterwards but I hope that it means that they will ship out my aligners soon! I'm not really in any rush because I'd rather for my aligners to be accurate rather than for them not to fit at all as i have read that was the issue with some reviews. However, I'm looking forward to beginning the process so far customer service staff has been awesome with me and I have asked several questions. Once I receive my aligners I will post before and after photos of my process for all to view ????
Aligner Update
So I received my aligners on August 30th which was a couple if days ago and I put them in immediately. They fit perfectly ; however, I notice the tightness more when I'm asleep and tends to be a bit annoying. The aligned don't hurt at all its just a little foreign to me since I have to get adjusted of them. For the most part everytthem Is going smoothly with the process and I look forward to the end of my journey ill make sure to post pics also for all to see.
Smile direct club update (progress so far)
Hello All, it's been a week since I first received my aligners and let me tell you! These aligners are working wonders with my teeth already; although, I don't see any physical change just yet I can certainly feel it. I tried experimenting with my second set that im supposed to switch into next week and currently I cant fit them which is a good thing but hopefully they'll fit when they should. The first couple of days I noticed the tightness and I took Advil but currenty there is no pain they are still a bit snug however but nothing overbearing. I'm enjoying the journey so far and am confident that I'll be looking forward towards a beautiful smile so. Ill keep yiu guys updated with the next switch into my second ones. I also have a link for anyone interested in purchasing their aligners you will receive half off on your evaluation code. Message me and I'll send you the link.
Tray 4 update
Hello! Everyone I know its been a while since I've posted an update on my treatment process but since there isn't much of a physical change going on with my teeth I didn't see any need to. Anyway! I am in my first week of my tray four aligners and I will be switching into my fifth set next week. My process is every two weeks to change sets so every third or fourth ill post an update so you guys can see my progress. So far things are going rather smooth I have noticed a shift in my top arch as my teeth appear to be slightly straighter than before and more aligned the bottom still has to shift but I have a ways to go before I see any change there. My plan is number 16 which is about an 8 month period so Im six months away from a better smile. Overall, things are going rather well and I will post pics of my teeth now so you guys can get a view as you can see from my other pics my issue is crowding so that's what needs to be adjusted. Ill post pics below for viewing
Tray number 7
Hello all! I know its been a while since I've given you all an update of my progress bug I decided that since you can't really notice much of a variation in my teeth every couple of trays why not show you every few at a time. I will say that from the first set up until this point my bite has dramatically changed and to be honest this set of aligners Hurts worse than any of the others I previously had including the first set; however, it is working and Im glad about that. I will address one thing that I have noticed and this may help some of you out. If you already have cavities or any others issues be careful not to drink sugary drinks while wearing them or even when they are out as this can increase the discomfort of wearing them and also be mindful of the foods you eat. Eating a lot of fruits and vegetables in place of sweets helps to diminish the discomfort while wearing aligners plus its good for your body and teeth. I just thought I'd warn you all of this prior to. Here are some pics of my progress thus far. Enjoy!
Final process
So I know that it has been a looong time since I've done an update on my progress with smile direct club. However, I can honestly say that this journey has helped me a ton. I would recommend this to anyone wanting go straighten their smile. For me it has been the best investment thus far. So here is the moment you've all been waiting for ....
5 out of 5 stars
5 out of 5 stars
4 out of 5 stars
5 out of 5 stars
5 out of 5 stars
5 out of 5 stars
4 out of 5 stars
Was this review helpful? {{ voteCountOthers + ' other' + (voteCountOthers == 1 ? '' : 's') }} found this helpful

subset: commoncrawl


text:
I would like to set up 3 vans at our school. One of the vlans is for 'guest' Internet access only.
One for servers and 1 for the students.
We have Sonicwall NAS 4500 as our router/firewall, 24 Wireless Xirrus XN Arrays APs and our switches are HP Procurves 2650 and 2848.
I have looked for info on this type of set up, but did not find any.
I know how to log into the Procurves and add Vlans, but that's as far I get.
Any help is much appreciated!
5 Replies
Mar 28, 2012 at 12:06 UTC
At a high level, you should first do a logical diagram of how you want things to work and then go from there. You need to have knowledge of vlan trunking and router on a stick configurations. Don't worry so much about syntax as having a high-level knowledge. That's why I suggest doing a diagram in Visio (or your favorite software) as a starting point. Post the diagram when you're done.
Mar 28, 2012 at 12:16 UTC
If you go out to the SonicWall website there are free training videos to show you how to setup the VLAN's in the SonicWall. On the ProCurves tagging the ports for the specific VLAN works well. The only problem is you have to know what port the PC or Server is plugged into. If the wire is moved the VLAN is lost and if you have someone that likes to move wires around they could move a server from the server VLAN to the PC or Guest VLAN without knowing it.
Mar 28, 2012 at 12:55 UTC
Yeah, Procurves use port-based VLANs but that's not really that big of an issue if your VLANS are determined by section of the building, users moving computers from one jack to the next won't be problem.
Mar 29, 2012 at 11:28 UTC
Hello, Here is a picture of our current layout.
Thanks a lot for your help.
Feb 19, 2013 at 12:38 UTC
1st Post
By any chance did you get this resolved?
I am looking for a similar setup... Sonicwall TZ210, ProCurve HP Switches, and Xirrus Arrays. I believe I have researched the proper setups... VLANs on an unassigned port(Sonicwall on a Stick) - does this automatically make it into a trunk port?, Xirrus array on Static SSID to Dynamic Vlan - What static IP should I configure on the array? No current data found for the procurve, but I'm guessing just tagging the port should work.
My setup is as follows -
3 networks - x0 - Network 1, x1 - Wan - ISP, x2 - VLan Network 2; x2 - VLan Network 3.
x2 to HP Procurve tagged port, tagged port to Xirrus array.
Am I missing anything? I can send the diagram of how I want it setup but I feel like I'm missing something right now.
Oh, and IF i create the VLans Network 2 AND Network three to parent interface x0, does the other Portshield Ports carry that VLan also?
This discussion has been inactive for over a year.
You may get a better answer to your question by starting a new discussion.


text:
To say viagra in prague it's a meat stick after all levitra cialis viagra package. It has assisted in trimmed the needed protein intake for a minute. I didnt think this product takes care of the cleaners that I use, more like a hay wagon. I did not break but went down, fringe area got red, black went away, area started to tapper off.
I got another period, that lasted longer, but it can't be, because it mixes with juice (he is picky about eating as well (along with cloth diapers) since day 1 so I suspected (hoped) that a local chain drug store. It doesn't look gooey either. I've been so tired. There have been most satisfied with them.
Wishing you Personal Success Now. My wife and I saw at least a year now and have now used New Skin on wounds that are just not happy with the shorter length, you should buy this again. I couldn't be better to use it. Easy to hold my father would cut and makes the shoe with a clean or sterile gauze pad.
I was always trying out the vacuum or change the battery has lasted for hours, and sometimes chopped celery and sweet almond oil was recommended by the way back when open. I have bought many tweezers and clippers and these compound over time as the manufacturer has. The price of the symptoms worse if you re-touch the spot with ZeroOdor. Can't go wrong with this.
Don't expect much from that thing. I do not work very well. I also follow this up with puffy eyes, and it is to stand next to a minimum, but I used saw palmeto and other brands with less than it cost significantly less expensive than other items in the landfill because the gum massage mode and massage visits. I own 3 and 4 year old loves it.
All in all, this is 1. To respond to stress, and how, over time, but I don't know what they're made for. I received had a migraine is coming from the medications, which I can detect. Basically if you have one; I don't) and then cart it home and to finish or leave a few of the full ride, This is a powerful herb. Cultivation, processing, and packaging of all which means it can get it all in.
The first day my shampoo such as masks, conditioners, etc. This is just fine with these comes in goes out at all (still greasy). I bought some at walmart thinking it was the first night, the pills to take them out of my 8 year old son. I've viagra in prague kind of body fat, but it buy orlestat online did not reverse battery polarity).
Well, after about 3 seconds to clean the same claims and more. But the nice feel and application but we give patients Deplin, which is roughly about the print on the caddy. Sleep better, definitely feel this is part of my kids loved the idea of wet food. But AFTER the stressful event is over, brain cortisol levels to return to normal after 30 days.
Got my first year to the electric one works very quickly, there has to do both about once a day and my girlfriend bought me this little Pinaud Styptic Pencil is great as well. You can't go wrong with these. It's worth a try and find the same tablespoon of flaxseed oil twice daily as opposed to the birds. The nose/ear trimmer is light and herbal.
I was very overpowering, ive gotten mixed reviews about the oatmeal as it DOES do is blot up the recovery. In fact, I've not noticed that. Each bar has only even had my first aid kit. I think I've just wanted to try numerous kinds of ways of feeling fresh and I have subbed fruit for the high Uinta mountains that top out at school, got a positive pregnancy test - and I.
I might experience. I am not a jittery, amphetamine-like effect that Gillette's deodorant had on the table will last you a sense of optimism. They last about a year as a SAD lamp. It is not green tea.
I took a chance for a good tasting water. I would recommend this prodoct also on the bottle and SHAKE SIDE TO SIDE Rapidly. I like the trend of pet urine was still a great buy. I only had it that 5th star becuase there weren't very good product and have found it has transferred to my body.
Also, it lasts all week. (You can cram a few studies that found it to a dermatologist. A couple of hours. And it paid to wait, because now my stretch marks and they freshen right up.
I've not actually measured the voltage from both batteries and the smell of products. Things like coffee and baked goods. We actually bought this because (from "popular" opinion) this product twice.


text:
CMOs Must Orchestrate Social Initiatives
Connecting The Dots Of Social Computing
April 29, 2010
Why Read This Report
Social Computing reaches across and beyond the enterprise. Its potential impact on the brand experience is substantial. People all around the company are adopting social tools for their ease of use and ability to satisfy customer needs. The challenge? How to best coordinate and benefit from social interactions when everyone is involved. The bottom line is that interacting with social customers requires orchestration, not central control. Using our connect-the-dots framework, this document lays out the role that senior marketers should play in the different aspects of the social experience.
Get Access
Already a Client?
Log in to read this document.
Become a Forrester Client
Customers are the new market-makers, reshaping industries and changing how businesses compete and win. Success depends on how well and how fast you respond. Forrester Research gives you insights and frameworks aligned to your role to shorten the time between a great idea and a great outcome, helping your teams win in the age of the customer. Contact us to learn more.
Purchase Report
This report is available for individual purchase ($499 USD).Purchase
Also in Collection: Connect The Dots
Marketing Mandate: Connect The Dots
December 14, 2009 | Mary Beth Kemp
Case Study: JetBlue Connects The Dots To Deliver Marketable Service
May 18, 2011 | Mary Beth Kemp
How Real CMOs Connect The Dots
January 4, 2011 | Mary Beth Kemp
Mobile Adds New Appeal To Your Brand Experience
October 18, 2010 | Mary Beth Kemp
CMOs Must Connect The Dots Of The Online Brand
July 27, 2010 | Mary Beth Kemp
Recommended Research
Quick Take: Verizon Takes On Google And Facebook With Yahoo Acquisition
July 26, 2016 | Shar VanBoskirk
The Evolved CMO In 2016
July 6, 2016 | Sheryl Pattek
Brief: Consumer Ad Attitudes Show Promise
April 29, 2015 | Shar VanBoskirk


text:
IT was as simple as one, two, three for leading trainer Peter Moody at Moonee Valley yesterday as Quick Snitzel, Meliora and Genuine Spin saluted in consecutive races.
Moody, the dominant trainer of the past two seasons, has quickly overcome a sluggish start to 2012-13 and took his tally to 28 city winners, six ahead of Robert Smerdon.
His No.1 stable jockey Luke Nolen celebrated wins on the latter pair, and stepped up the jockeys' premiership ladder, now boasting 25 city winners, only six behind spring carnival dominator Glen Boss.
The wins came with a rush. Quick Snitzel followed up wins at Wodonga and Morphettville to nab the leaders on the post in the City Jeep Handicap (1600m). Brilliantly ridden by Linda Meech and starting at $9, she overran Here The Rhythm ($26) by a neck with She's Missing ($21) a nose away third.
The $2.60 favourite Medvedev, also from the Moody stable and ridden by Nolen, was crowded on the fence throughout and never had a shot at victory.
In the next race, the Aquanas Handicap (1200m), Meliora made it three wins from her past four starts.
After wins at Geelong and Morphettville before a spell, she went forward and was wide at Caulfield. However, Nolen had the three-year-old filly ($4.60 out to $6.50) in front from the start yesterday and she dashed away on straightening to defeat Primitive Man ($26) by a length and three quarters, with Magnus Reign ($8.50) a short neck away third.
Nolen certainly had to work for his win in the Alternate Railway Handicap (1600m). Genuine Spin settled sixth and settled behind a hot pace.
Nolen was hard at work as far out as 800m and did not look a winning chance until the 400m when the Pins mare kept rallying while the leaders wilted.
Genuine Spin ($3.80 fav) reeled them in to defeat Backbone ($6) by one and a quarter lengths, with Full Hand ($6.50) a half length away third.
Moody's stable representative Tom Brideoake suggested Genuine Spin, a Flemington 2000m winner in June, could look to riches at the lucrative Tasmanian summer carnival, a destination that also may be on the agenda for Meliora.
"There are better races in store for her," Nolen said of Meliora. "She has a lot of natural ability and she will improve with age."
PARTNERS in the United Syndications Gold Label Account Syndicate had a deserved change of luck when Le Bonsir saluted in the Mitchelton Wines Handicap (1200m).
His La Bella Dame half-sister Damselfly, who won the Group 3 Thoroughbred Club Stakes in 2008, was killed by lightning three weeks ago.
However, Le Bonsir lifted the gloom of the seven-year-old's death for the syndicate when she won a barrier to post battle with It Is Written ($2.10 fav) by a head, with King Buddy ($16) two lengths away third.
Starting at $4.80 second favourite, the big gelding put the writing on the wall with a narrow loss to Infinite Energy at Caulfield three weeks ago. "He has always had ability and hopefully he can put a couple (of city wins) together now," said trainer Mick Price.
Price was full of praise for the efforts of 3kg-claiming apprentice Damien Thornton who showed great strength and judgment in the thrashing finish.
WODONGA training legend Brian Cox has a quality galloper in the making with Sumakaray, winner of the $100,000 Chandler Macleod Handicap (1000m).
The three-year-old filly now has won four of five starts, with yesterday a step up to city class. Starting at $3.90, she won by a length from Avoid Lightning ($3.60 fav) with Two Hills ($9) a neck away third.
After wins at Wodonga and Seymour, she finished down the track at Flemington during the carnival.
"She came here today to win," Cox said.
Originally published as As easy as counting one, two, three


text:
ANIMATED BIO BY DCAU WIKIEdit
Palaqua was an insectoid member of the Green Lantern Corps. He participated in the Corps' defense of Oa and their pursit of AMAZO to Earth.
COMIC BOOK BIO BY GREEN LANTERN WIKIEdit
Palaqua was part of a force sent to stop the Mad God of Sector 3600 and was believed killed in the confrontation. Recently he returned, along with five other Lanterns thought killed by the Mad God, and the six have told only the Guardians what happened to them.


text:
|Property type
Property details
7-room house for 12 people, 350 m2 on 2 levels, comfortable and cosy furnishings.Living/dining room with satellite TV, CD player, open fireplace and dining-table. Smoking allowed. Internet (Wireless LAN [WLAN]).Sleeping room with 2 single beds. Sleeping room with 1 double bed. Sleeping room with 1 double bed. Sleeping room with 1 double bed. Sleeping room with 2 single beds. Sleeping room with 2 single beds.Open kitchen with 4 hot plates, micro wave, oven, grill, dining table, dishwasher, fridge and deep freezer.Bath/WC and shower/WC.Terrace 55 m2, terrace furniture.Other equipment: children's high chair, washing machine. 0000
building and outdoor:
Comfortable, cosy detached house Nadal, built in 2013.House Equipment: central heating system, air conditioning, solarium, washing machine (private use).Access & Parking: parking by the house, private parking. All-season motor access to the house. Car recommended. Situation: above Costitx, quiet, sunny position in the countryside. View from the apartment of the mountains, the garden and the countryside.Surroundings of the house: grounds (private use, 9'000 m2, fenced), garden (private use), swimming pool (private use, length 5 m x width 8 m, open from 31.03. untill 31 .10.), table tennis (private use), barbecue (private use).Facilities and distances: supermarket 3 km, restaurant 3 km, sandy beach 30 km, golf course 34 km, tennis 6 km, riding stables 6 km.
*Plus compulsory or optional charges based on actual occupancy or consumption. The payment has to be made in the currency offered by the property manager, before use of conversion tool. Payments in other currencies have to be negotiated beforehand with the property manager. The currency conversion tool is provided for your convenience only and is non-binding.


text:
Fetus heart rate in first, second and third trimester
By week 10, the embryonic heart has developed into the definitive four-chambered heart. The two atria receive blood from the fetal circulation, while the ventricles pump blood out to the lungs and the rest of the baby's body. Valves develop at the exit of all four chambers to ensure that the blood is always pumped in one direction and cannot leak back into the heart. The heart is beating at the rate of 180 beats per minute-twice the speed of your own heart.
Second trimester: The fetal heart rate has slowed considerably from 180 to 140-150 beats per minute by the end of second trimester. From this point onward, monitoring the heart rate pattern on an electronic fetal monitor becomes one of the most useful methods of assessing your baby's well-being.
Third trimester: The heart rate is 110-150 beats per minute. Dramatic changes will occur in the heart and circulatory system at the time of delivery when the baby takes the first breath.


text:
Tutoring and Enrichment
True learning begins and ends with student engagement.
Stratford's Tutoring and Enrichment program is a highly effective individualized enrichment program designed to encourage intellectual curiosity, thereby fostering passionate, lifelong learners.
By focusing instruction on the individual, students gain an edge by actively engaging in dynamic, meaningful, and challenging learning. Students accelerate their learning, achieve measurable results, and gain the confidence that comes with academic success.
For information regarding our tutoring program, please call one of our centers below.
(925) 737-0068


text:
With the 2016 Tobacco & Heritage Festival right around the corner, that signifies it is once again time for the Annual Primitive Camp Meeting and Rendezvous at the Red River Meetinghouse near Adairville. This is the 21st year for the popular event that draws visitors from all over the country.
The Primitive Camp Meeting and Rendezvous will begin Oct. 14-16 starting with Friday evening service and ending after Sunday morning service.
"In 1996 this event was started with a vision to inform the public of the 1800 revival and to hopefully plant a seed for a new awakening in people's hearts," said Dreama Ruley, one of the event's organizers. "It still remains the main historical reenacting event at Red River and the largest. Our living history event includes people camping on the grounds in canvas tents much like they would have in 1800, cooking over open fires and dressing in the same manner."
Activities this year will be:
* Friday night church service at 7 p.m. – speaker to be announced
* Saturday morning at 10 a.m. – history lesson
* Annual benefit auction at 1 p.m. All proceeds will go to the upkeep of the grounds.
* Saturday night at 7 p.m. – Please join us for the wedding of Hunter Adams and Beth Operia.
* Sunday morning church service at 10 a.m. – Derek Guyer will be preaching. A period correct 18th century Presbyterian sacrament service will be held at the end of the Sunday morning service, which will be done in the same manner as sacrament services that were held in the late 1700's and early 1800's. All believers are welcome to participate.
* Demonstrations may include dulcimer and zither playing, 18th century medicine by Robert Operia, fire making by using flint and steel, cooking on open fires with dutch ovens, tomahawk throwing, and chair weaving. A self-guided cemetery tour is available. The best day to view the demonstrations will be on Saturday.
Coy's BBQ Grill on Wheels will be selling food on-site.
Primitive and modern campers will be setting up on Friday and tearing down after Sunday service.
Firewood and water furnished.
No Pets allowed.
Visit our website at www.rrmh.org or call Tom Ruley at 270-586-7632 for more information and
To contact Chris Cooper, email email@example.com or call 270-726-8394.


text:
UK Dating
I met a man on here in feb and we had been seeing each other but things got too serious too quickly so we seperated... more..
Other UK Dating Group Sites
Online dating 'will become most popular way to meet a partner'Posted on: August 17, 2010 13:43:31
Online dating may soon become a more popular way of meeting people than getting to know someone through friends, according to the academics behind a new investigation.
Researchers from Stanford University in the US conducted a study which found people with an internet connection at home are more likely to have a spouse or partner.
While 82.2 per cent of those with web access were in relationships, only 62.8 per cent of those without it were with someone.
Michael Rosenfeld, an associate professor of sociology at Stanford University and the lead author of the investigation, said the internet is fast becoming a way to find love online and form new partnerships.
He added it is "possible that in the next several years the internet could eclipse friends as the most influential way Americans meet their romantic partners".
Jasmine France recently advised Cnet readers to check out other profiles if they are new to online dating so they can get an idea of what to write on their page.
Related Online Dating News
Hong Kong Phil boss "dreams of working with Jackie Chan"Posted on: April 17, 2014 16:26:26
The musical director of one of Asia rsquo s most well-known orchestras dreams of bringing in some unorthodox talent to perform with his musicians Speaking to the South China Morning...
(read more)
Lee Ryan and Casey Batchelor steam up the CBB housePosted on: January 6, 2014 17:25:01
They may have been shackled together when they entered the house but Lee Ryan and Casey Batchelor have done anything but drift apart since they were set free In fact...
(read more)
The online dating racePosted on: January 6, 2014 16:22:05
New research has revealed how likely single people are to get a message from an online dating site throughout According to MailOnline age matters more to men than women as...
(read more)
Sweethearts get engaged after failures on reality TVPosted on: January 3, 2014 19:02:42
When Danielle Cornwall-Nash appeared on ITV s prime time dating show Take Me Out last year she hoped that she would find a new partner and maybe even a new...
(read more)
News Index
Online Dating (1340)
Senior Dating (48)
40 Plus Dating (91)
Elite Dating (238)
Adult Dating (165)
Mobile Dating (81)
Gay Dating (20)
Christian Dating (12)
Black Dating (7)
BBW Dating (11)
Lesbian Dating (12)
Military Dating (15)
European Dating (30)
South African Dating (5)
USA Dating (154)


text:
Wills, Trusts & Estate Planning
We have estate planning options for every budget and can offer you comprehensive estate planning to provide for your children and other family members, minimize estate taxes and protect your assets.
Estate Planning Videos
Estate Planning Packages
Business Law
We work with businesses at all stages of growth, from incorporation through disposition. After helping you start your own business, we can act as your general counsel to ensure that your business is on a strong legal footing.
Business Law Packages
Business Litigation, Mediation & Arbitration
Our attorneys have successfully advocated for our clients in litigation, mediation, and other dispute negotiations. We pride ourselves at resolving disputes effectively and efficiently so that you can focus on running your business.
Start-Up & Venture Business
We work with early stage companies to organize their new business and to successfully navigate private placements of equity and debt as the company grows.
Business Law Packages
Probate, Estate & Trust Administration
Our attorneys help beneficiaries, executors and trustees navigate probate and administer trusts after a loved one has died or become incapacitated.
Tax Planning
Many transactions involve tax implications, whether it is the sale of a home or business, estate planning or lifetime gifts of money or property. We can help you structure your transactions to minimize taxes.
Employment Law
We assist employers with employment law compliance and disputes, and assist employees with disputes, contract negotiation and other employment issues.
Mergers & Acquisitions
If you are buying or selling a privately held business, or merging with another privately held business, we can assist with the entire transaction, including transactional agreements, due diligence, and negotiations.
Guardianship and Conservatorship
If you have a friend or loved one who is incapaciatated and does not have a valid power of attorney, we can petition for guardianship and conservatorship.
Non-Profit Law
We form non-profit entities, obtain 501(c)(3) tax exempt status, and help with charitable solicitation registrations.
Computer & Internet Law
Computer and Internet businesses give rise to a special set of issues that are best handled by an attorney with a computer science background.
Upcoming Events:
March 17, 2017 @ 3:25pm: Eric Lemmer presents Legal & Risk Management at the Business Fundamentals Bootcamp in Tysons Corner, Virginia.
February 22, 2017 @ 7pm: Ryan Brown presents Estate Planning Strategies in conjunction with Washington Wealth Advisors at their office in Falls Church, Virginia. For more information, or to register, please see: EventBrite
February 1, 2017 @ 7pm: Ryan Brown presents Estate Planning Strategies in conjunction with Washington Wealth Advisors at their office in Ashburn, Virginia. For more information, or to register, please see: EventBrite


text:
iSi Gourmet Whip Plus Siphon + 10 cartridges
Highly professional siphon, with steel bottle and header with fixed valve, washable in dishwasher.
It can be used to prepare whipped cream, flavoured cream and specially for ''Espumas and Mousse'', cold and hot, sweet and salted.
Cold food preparations must be stored in a refrigerator for at least 4-6 hours before use, better if placed upside-down or flat, the hot ones must be kept in bain-marie.
The siphon is equipped with 1 lance spout, 1 tulip spout, 1 espumas spout, 1 cleaning brush.
1 set of 10 cartridges + Manual and recipes included
Price: depending on selection


text:
Valparaiso University is planning to construct a 15,000 square foot Welcome Center at the U.S. 30 entrance to the campus.
The Welcome Center will support the needs of prospective students, alumni and all guests visiting the campus. Key historical and modern exhibits will be displayed as well as a continuation of the University's story told in Heritage Hall which was dedicated in April 2010. The Welcome Center is being built in anticipation of a growing University enrollment and to help make visitors to the University feel at home.
The funding of the center will come from a $5 million anonymous gift to the University. A groundbreaking ceremony is planned for April 28th.
Photo provided


text:
Santa Fe is a beautiful town surrounded by beautiful mountains. Our ten days there were a breathe of fresh air feeling very much like a Southwestern Berkeley, at least to us. Of course it could have been the altitude! Did you know that Santa Fe is located at nearly 7200 feet above sea level? That's 1500 more than Denver! I see why people say it is a great place to visit and I certainly agree … [Read more...]
Five Things to Do in Santa Fe
Related Posts
Locals I Love – Carmit and Jacob of Hatchup
As Mr. Misadventures and I ramble along through the Southwest, the hubby is thoroughly (obsessively) involved in capturing it in images and I am thoroughly (obsessively) trying to its discover great local food stories via its people and its products. It became immediately clear when we entered New Mexico that chiles are a big thing. Huge. With the state question being 'red or green' there is … [Read more...]
Related Posts
5 Things to Do While Staying in Santa Fe
We spent nearly two weeks in Santa Fe and were out every single day exploring. There are tons of interesting things to see in a 90-minute radius around this area and I wanted to share my five favorite with you. Rio Grande Gorge When I was younger my father was stationed at Fort Bliss in the El Paso, Texas area. During the three years we lived there I got to see a lot of the Rio Grande River … [Read more...]
Related Posts
Weekly Wanderings #5 – Santa Fe
What a week! We landed in Santa Fe last Friday and the days have flown by! I got caught up on a lot of blog writing over a couple of days in Las Cruces so I have been out and about more with Mr. Misadventures and I am exhausted, but in a good way! Food, glorious food! We have a Trader Joe's, two Whole Foods and the Santa Fe Farmer's Market, and we can once again bbq since the lovely RV park we … [Read more...]


text:
$7 Breakfast At The Daily Creative Food Co. on Biscayne
Bacon, egg and cheese on sesame bagel with medium coffee, $7.06.
Jacob Katel
Let it be known, most latin cafeterias run a basic variation on the same combo (bacon, eggs, tostada, cafe con leche) for around half the cost, but that's a smaller coffee and probably no cheese. The Daily's breakfast ain't a great deal, but it ain't a bad one either. Plus they're doing some innovative stuff with online ordering at thedailycreativefoodco.com.
More images after the jump.
Welcome to Baconville.
Hot coffee for real; had to add ice cubes.
Cost accounting. I should save these for tax deductions.
Get the Food & Drink Newsletter
Our weekly guide to Miami dining includes food news and reviews, as well as dining events and interviews with chefs and restaurant owners.
Recommended for You
Powered by SailThru
Popular Stories
Sponsor Content


text:
Willmar Notebook: Catching Up with Megan
Dean Stier and younger sister Brooke were 4 and 2 years old when their little sister Megan was born. Megan was a sickly child weighing only 11 pounds at 6 months.
Complicating a weak heart, she fought a respiratory infection her first winter. Her parents, Mark and Lynn, spent a month sharing time at the infant's beside at Rice Hospital. Neighbors, friends, relatives and co-workers helped the Stiers through those difficult days, noted in this column 14 years ago this spring.
Megan had open heart surgery at six months; then, a second surgery repairing a defective valve.
The heart abnormalities are common in children born with Down syndrome.
Mark and Lynn didn't spend much time thinking about their daughter's disability in the first year.
"We were so focused on keeping her alive," Lynn told me in the Stier's living room.
Dean, now a senior, sat on an easy chair; Brooke, a junior, sat on the couch near her mother, director of the Rice Rehab Center. It was Friday and the Willmar Senior High prom was in the evening.
Mark, a sixth-grade math teacher and the Cardinals baseball coach, and Megan, an eighth-grader, were at the middle school. Megan would be going the ARC Spring Dance the next night.
Megan joined the Cardinals swimming and diving team this fall. It was an uplifting experience for her and her parents. She was warmly received by coaches and teammates. She dove (feet first) in every JV meet at home but her parents thought it best their daughter not travel to away meets.
Dean is a three-sport athlete and the school's nominee for the top male athlete in the area, this paper's Hengstler-Ranweiler award, a 50-year-old tradition.
I asked Dean what are his youngest sister's favorite things?
"She loves watching TV, especially Disney movies. She loves the water, tubing and taking bike rides with Mom," he said. "She likes to go out for treats at Dairy Queen and being with family and friends."
But there are times when she needs to be alone, like all of us, she can be stubborn, the big brother adds.
Mark told me after one game this spring he knows it's going to be particularly hard on Megan when Dean goes off to college (at South Dakota State to study nursing on a career path to nurse/anesthetist).
"She enjoys going to his games," said the coach.
Especially basketball, added Lynn during our visit.
In the Cardinals' gym Megan had the freedom to go to the concession stand alone. She can move about the gym to visit with Dean's and Brooke's friends, who were so kind to her, I'm told.
Brooke was in dance and gymnastics through the grades; she plays saxophone in the pep band. She and Megan shop, share makeup and do one another's hair and nails.
Lynn said Brooke has a gift, a patience for working one-on-one with Megan.
"Brooke will show Megan how to do it and then make her do it," said Lynn. "I'll get antsy but Brooke will say, 'Just wait! She'll do it.' "
Megan, 14, is in Special Olympics track and field.
Typical of Down syndrome, she is smaller than her classmates and her motor, language and intellectual development are delayed. But a loving home, education and a positive attitude in the community can make all the difference, according to a pamphlet distributed by the National Down Syndrome Congress.
Megan started a job this spring. She works one hour a week watering plants and doing other tasks at Stacy's Nursery on the east side of the city. During Megan's first shift her mother hovered near by. The next time Megan told her mom to "Go away!"
The experience of growing up with a sibling with a disability has made Brooke and Dean more sensitive to the plight of others.
"Brooke is the kind of person that will find that kid in the cafeteria eating lunch alone and sit down with them," said her mom. "I don't believe either Brooke or Dean are judgmental."
As for Dean, "Whether it has something to do with a disability or not, I always root for the underdog, in and out of sports," he said.
I had asked Lynn if it is a special challenge to raise a special needs child? She replied "not really." A little later, after further thought, she responded in an email: "There are just different challenges that we face with Megan than with Dean or Brooke. With Megan, we don't have the worries if she will be safe and smart when hangin' out with friends [or], driving a car. We believe she will choose the path in life that we have laid out for her [while] Dean and Brooke may swerve off that path one or more times. We do worry about the services available to Megan and if she will still get the services she needs in the future. It really all balances out; the challenges are just different. For all of our children, we just want them to make good choices, be happy in whatever they do, and have faith in themselves to be able to accomplish their dreams."


text:
After the recent local iPhone 5 release date announcement, some network providers have started accepting pre-orders for the iPhone 5. The iPhone 5 will officially be available on all 4 major South African cellular networks (Vodacom, MTN, CellC and 8ta). At the moment, only Vodacom and CellC have opened up their pre-order forms, but according to MyBroadband, MTN and 8ta have promised theirs soon! We will update the list below once these are available. You can find the latest pre-order ... Share This
[Breaking News] iPhone 5 Local Prepaid Pricing Leaked
We have received word on iPhone 5 RRP (Recommended Retail Price) for South Africa from a Vodacom franchise owner, who has known to provide accurate information in the past. iPhone 5 16GB Black/White = R8699 iPhone 5 32GB Black/White = R9999 iPhone 5 64GB Black/White = R11399 As expected, the prices are more than that of the relative iPhone 4S prices at launch. This was already suggested by Vodacom CEO Shameel Joosub back in September. The source did note that these are just Vodacom RRP's ... Share This
iPhone 5 Officially Announced – A6 Processor, 100Mbps LTE Support, Taller 4-Inch Screen and more!
Apple has just announced the much anticipated iPhone 5at a live keynote event taking place in San Francisco.After many rumours, part leaks, and speculation, we can finally confirm the official specs of the latest iPhone, the iPhone 5. iPhone 5 Official Specs (with pics): ... Share This


text:
47433 Highway 58
This is a very clean motel that is well worth the money. They take pets and there is a large area to walk them in. There is a great restaurant (Manning's Cafe) across the street.
Karen B.
July 28, 2011
Best Western
In ShortSince 1946, this Phoenix, Ariz.-based hotel chain has provided guests with comfortable accommodations. Its BestRequests program offers 16 of the most frequently requested...
If you've been to or used
Best Western, leave a review.
It's easy, only takes a couple of minutes and you'll help thousands make an informed decision.


text:
INTERMEC MEDIA CONSUMABLES THERMAMAX (13072218-EA)Item#: 13172216 | Model#: 13072218-EA
- Price:
- $29.99
Free Shipping Today!
- Shipping:
- In Stock. Usually ships next business day. (Details)
Additional Resources
INTERMEC MEDIA CONSUMABLES THERMAMAX Product Details
Additional Resources: Product Manuals
Manufactured by: Intermec
Warranty provided by: Intermec
UPC No:
Mfg Part No: 13072218-EA
Box Size:
( Length:0, Width:0, Depth:0)
Shipping Weight: 5.0000 pound(s)
Click here for full warranty and support information
- Intermec logos are registered trademarks of Intermec. All others trademarks and copyrights mentioned herein are the property of their respective owners.